This file is indexed.

/usr/bin/mcrl2compilerewriter is in mcrl2 201210.1-1ubuntu1.

This file is owned by root:root, with mode 0o755.

The actual contents of the file can be viewed below.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
#!/bin/sh
# Author(s): Sjoerd Cranen
# Copyright: see the accompanying file COPYING or copy at
# https://svn.win.tue.nl/trac/MCRL2/browser/trunk/COPYING
#
# Distributed under the Boost Software License, Version 1.0.
# (See accompanying file LICENSE_1_0.txt or copy at
# http://www.boost.org/LICENSE_1_0.txt)
#
# This script is the default script to compile rewriter
# libraries. It is generated, so to change compiling
# behaviour, follow the following steps:
#
# - Create a new script (perhaps based on this one)
# - Let the MCRL2_COMPILEREWRITER environment variable
#   point to the new script.
#
# Requirements for a compile script: the output (both
# stdout and stderr!) must consist solely of a newline-
# separated list of files. The last file in the list is
# treated as the compiler library, and must be a valid
# executable. All files listed in the output are deleted
# once the rewriter library is no longer needed.

(echo $1 &&
/usr/bin/c++ -c -O3 -DNDEBUG -std=c++98 -DNDEBUG -m64 -DAT_64BIT -fPIC  -I"/usr/include" -I"/usr/include" -o $1.o $1 > $1.log 2>&1 &&
echo $1.o &&
/usr/bin/c++ -shared  -o $1.bin $1.o >> $1.log 2>&1 &&
echo $1.log &&
echo $1.bin) || (
echo "Compile script was:" &&
cat $0 &&
echo "Compilation log:" &&
cat $1.log)