satyr: minor refactoring in the parser / translator classes

Change-Id: I2be96b257bbd037ba1abfde072d239352e391af4
undertaker: quickfix for ',' in filenames

Some new files in the current linux head have ',' in the filename and
the CNFBuilder cannot parse these files. Thus, normalize_filename is
expanded to replace ',' with '_' like it's done with other chars.

Change-Id: I9d016f51a76adbe4e21863b75e497ca712a66623
doxygen: upgrade to an newer doxygen file using "doxygen -u"

Change-Id: Ied7cefb84df773ceb0a825b727482e4f80dca357
undertaker: minor refactoring in satchecker and conditionalblock

The format-Methods of Satchecker::AssignmentMap should be callable on
const references or pointers, since they are just formatting the state
of the AssignmentMap differently without altering the state of the
AssignmentMap.

Change-Id: Iafc6f867ea4eca8e27603aa003635d45158de3ae
undertaker: fix deprecated warnings from bison when building BoolExpParser

Change-Id: Idb4a7ad42d9ec43f7d419ffbc2724b4c2e74c4e8
Revert "undertaker/predator: time-out only for long running jobs"

This reverts commit 66df6b70348648f47377a6902f319c90397daf17.

While this Change wasn't a problem on normal .c files, there are
several .h and .S files which cannot be parsed by puma and might lead
to unexpected behaviour to end users.

offending files: include/linux/skbuff.h and several headers containing
asm macros.

Change-Id: Ic459334825cbf03d1a48a9b3cf83095df8a57479
undertaker: cleanup global RETVALUE and exit child-processes correctly

With commit 444baab54cfc4a2c33c49b6b9219257e901c87a1, the global
variable RETVALUE was set correctly within child-processes and the
exitcode of these processes indicated an error if there has been one.
However, this lead to an subtle bug:
Since RETVALUE is global and wait_for_forked_child sets RETVALUE to
EXIT_FAILURE if a child-process had an exitcode != 0, all
child-processes started after the first error, had EXIT_FAILURE as
exitcode, even if they were processed correctly.

This change removes the global RETVALUE variable and ensures,
child-processes will have the correct exit value.

Change-Id: Ic5f2e475f14a290bcccce5cf23ac9c7e1678d4f2
undertaker/golem: normalize inference symbols in golem

We normalized the filename of the analyzed files in several places
within our code. This made our code not just harder to maintain but
also inconsistent:
The CNFBuilder (to be more precise, the BoolExpParser) has problems
with several chars (like: ":+/,-") in symbols within formulae and
fails.
When we transform the inferences for CNF-Models in rsf2cnf, we had to
normalize the inference symbols (which identify the filename to which
the formula belongs) and store that normalized symbol in the model.
However, in RSF based models, we just append the inference formulae to
the model, which leaves us with two different ways of storing
inferences in the models and more complicated code.

To fix this, "golem -i" now prints the normalized filename (the path
to the file is still recognizable) and undertaker normalizes the
filename _once_ when the normalized file-Variable is accessed through
a getter method from the CppFile-Object.

Change-Id: I52cff842fc8cd1fbb42543713d912c5111c5b38e
scan-head/linux-tree: cleanup shellscripts and make them less verbose

With the proper progagation of ret-values within undertaker,
dead-analysis almost always returns with an exitcode != 0 on a
worklist covering the whole linux tree.
(Explanation: some files just cannot be parsed by puma (.S), some
formulae cannot be properly parsed by the CNFBuilder(value symbols))

If an error occurs, undertaker-scan-head dumped the whole error-file
into stdout and continued. The error-files are now moved to the
result-directory and can be inspected if needed, without dumping them
before.
(CNFBuilder errors often contained a huge formula, rendering the
output of undertaker-scan-head useless.)

Additionally:
- cppsym analysis was done parallel until now, what is not a good idea
  without synchronizing the output.
- 'set -e' was removed from these shellscripts. This option is
  considered bad style and silently exits the shellscript if a called
  program had an exitcode != 0, what is generally a bad idea for
  debugging these scripts.

Change-Id: Ief602e3e60cf2b344dd7ccd6f5343a5ef9fec9d8
undertaker: parallelize model parsing

After refactoring the PicosatCNF class, we are able to parallelize
model parsing before having a reentrant version of PicoSAT.
This is not a great deal for RSF-Models but is speeding up loading
CNF-Models to the same level as RSF-Models.

Change-Id: Ie0a50d915552b547b2ae1a8f458926b2128f1336
undertaker: introduce threadsafe logging

With variadic templates from c++11 we can implement our logger more
efficient and also threadsafe.

Change-Id: I754258ddaa1ed09ca5ca457a821b5c6cfe47039b
undertaker: remove standard boost::regex::perl from regex declaration

We don't have to mention the default regex-type boost::regex::perl
when we define a regex.

Change-Id: I7f3b7f77b6d06a4c34609e6f69af90157ed98f96
Merge branch 'master' of https://i4gerrit.informatik.uni-erlangen.de/p/undertaker