Bitvector and array literal support for Theta backend

[as3810t]

This pull request adds support for bitvector expressions and array literals in the Theta backend. Also as a minor improvement closes #37 .

• Bitvector support
• Array literal support
• Functional tests for the new features (Depends on this pull request in Theta)

[hajduakos]

ftsrg/theta#77 was merged

[hajduakos]

As far as I know, ftsrg/theta#77 only added syntactical support for bitvectors, besides --refinement UNSAT_CORE the other refinement algorithms do not really work. However, I am going to merge ftsrg/theta#82 soon, which will add new refinement algorithms. It would be nice to use them by default for bitvectors. (Currently SEQ_ITP is the default.)

[hajduakos]

PR ftsrg/theta#82 was merged, so Theta v2.4 has advanced refinement algorithms that support bitvectors. If #41 also gets merged here, functional tests could use these new algorithms.

[radl97]

Don't forget to enable testing theta with flat memory model:

Build result:

UNSUPPORTED: gazer :: theta/verif/memory/arrays1.c (15 of 102)
UNSUPPORTED: gazer :: theta/verif/memory/arrays2_fail.c (16 of 102)
UNSUPPORTED: gazer :: theta/verif/memory/globals1.c (17 of 102)
UNSUPPORTED: gazer :: theta/verif/memory/globals2.c (18 of 102)
UNSUPPORTED: gazer :: theta/verif/memory/globals3.c (19 of 102)
UNSUPPORTED: gazer :: theta/verif/memory/globals4.c (20 of 102)
UNSUPPORTED: gazer :: theta/verif/memory/local_passbyref1_fail.c (21 of 102)
UNSUPPORTED: gazer :: theta/verif/memory/passbyref1_false.c (22 of 102)
UNSUPPORTED: gazer :: theta/verif/memory/passbyref2.c (23 of 102)
UNSUPPORTED: gazer :: theta/verif/memory/passbyref3_fail.c (24 of 102)
UNSUPPORTED: gazer :: theta/verif/memory/passbyref4.c (25 of 102)
UNSUPPORTED: gazer :: theta/verif/memory/passbyref5.c (26 of 102)
UNSUPPORTED: gazer :: theta/verif/memory/passbyref6.c (27 of 102)
UNSUPPORTED: gazer :: theta/verif/memory/passbyref7_fail.c (28 of 102)
UNSUPPORTED: gazer :: theta/verif/memory/pointers1.c (29 of 102)
UNSUPPORTED: gazer :: theta/verif/memory/structs1.c (30 of 102)

The change would be deleting this file:

https://github.com/ftsrg/gazer/blob/master/test/theta/verif/memory/lit.local.cfg

(I think there was a change in these files in the PR)

@as3810t

[sallaigy]

Left some minor comments, but overall very nice work! Could you please take care of the following major things?

1. Reformat the code so it follows our existing convention:

if (c) { // Note that there is a whitespace between the keyword and the condition

} else if (d) {

} else {

}

2. Update the lit tests so that they will run the memory model tests with Theta (by removing the local lit configuration and the REQUIRES directives in the tests).
3. Update the existing unit tests for the new Theta expressions.

[sallaigy]

Is Theta able to handle this testcase with the flat memory model now? If so, this line should be remove (in all the other tests as well).