9557087b2e
Merge pull request #4577 from peterschrammel/do-not-expose-set-frozen
...
Do not expose set frozen [depends: 4573]
2019-04-27 21:14:43 +01:00
13f5f0c2a4
Do not expose set_frozen
...
Is only used inside the prop_conv_solvert hierarchy anymore.
2019-04-27 20:18:59 +01:00
a951d96d5a
Move handle() from interface to implementation
...
The implementation should be in the implementation class.
2019-04-27 19:23:31 +01:00
e37ef07ed8
Merge pull request #4573 from peterschrammel/conflict-provider
...
Split out is_in_conflict solver capability [blocks: 4577]
2019-04-27 19:14:33 +03:00
3e19c9168c
goto_statet cannot have a default constructor
...
It uses classes that don't have a default constructor. This change is
required for compilation with clang 8.
2019-04-27 16:45:38 +01:00
cdd8e6d659
value_sett cannot have default copy operator
...
It uses classes that don't have a default copy operator. This change is
required for compilation with clang 8.
2019-04-27 16:45:28 +01:00
8384ce3a4d
rename stack() macro
...
The macro clashes with std::stack. This change is required for compilation with clang 8.
2019-04-27 16:45:06 +01:00
e551a177ba
goto_statet cannot have default assignment operator
...
It uses classes that don't have a default assignment operator. This change
is required for compilation with clang 8.
2019-04-27 16:45:16 +01:00
56e798ef7f
symbol_table_buildert cannot have move constructor
...
It uses classes that don't have a move constructor. This change is required
for compilation with clang 8.
2019-04-27 16:45:06 +01:00
ef366e5a7e
Split out is_in_conflict solver capability
...
This is only provided by the prop_conv_solvert-based hierarchy
at the moment and is quite specific to MiniSAT-based solvers.
The functionality itself is used out-of-tree only (2LS).
2019-04-26 17:44:14 +01:00
b77b5b09d4
Merge pull request #4571 from thomasspriggs/tas/java_synthetic
...
Parse and convert the synthetic flag of java methods
2019-04-26 16:51:09 +01:00
176c960b66
Merge pull request #4572 from jeannielynnmoulton/jeannie/java_is_enumeration
...
Add getter/setter for ID_enumeration in java_class_typet
2019-04-26 16:38:45 +01:00
d706767983
Parse and convert the synthetic flag of java methods
...
For use in a downstream repository. This is used to indicate whether a
method was synthesized by the java compiler, as opposed to being a
method which has corresponding user written java code.
2019-04-26 15:35:39 +01:00
edccf7c82f
Add getter/setter for ID_enumeration in java_class_typet
...
Adding getter/setter to avoid direct irept access
2019-04-26 14:14:59 +01:00
385a27cf24
use static_members in Java frontend
...
An instance of static fields for Java classes. The Java-specific extension
enables tracking static fields that are final.
2019-04-25 08:08:38 +01:00
55c89cbfc4
introduce class_typet::static_members
...
This enables tracking static fields of a class, following the same pattern
as used for methods.
2019-04-25 08:08:38 +01:00
12a3d18fad
fix return type of class_typet::methods
...
This is likely a copy-and-paste error.
2019-04-25 08:08:38 +01:00
1b9bd934a0
Merge pull request #4568 from danpoe/refactor/use-forwarding-references-in-sharing-nodes
...
Use forwarding references in the sharing nodes
2019-04-24 20:07:35 +03:00
d79620a189
Use forwarding references in the sharing nodes
...
Previously there were two versions of some methods, one taking a const reference
and the other taking an rvalue reference. This commit changes the methods to
take a forwarding reference which allows to remove one of the versions.
2019-04-24 15:16:27 +01:00
189c1ad17c
C++ front-end: default constructed PODs are constants
...
We already supported single-argument construction, and explicit casts
already took care of zero-initialisation, so really all we needed was to
remove some code.
2019-04-24 13:13:11 +01:00
65fc001cd6
fix calls to validate_expr in util/std_code.h
...
The current calls use an expression; validate_expr(exprt) is a no-op. Using
the casted type enables the checks.
2019-04-24 13:00:49 +01:00
626ec18124
Visual Studio: silence warning about macro re-definition and conversion in lexer
...
Flex generates definitions before system headers are included, and tokens result
in signed/unsigned comparison.
2019-04-24 11:41:13 +01:00
9439180ef0
Silence Visual Studio warnings in generated parser code
2019-04-24 11:41:13 +01:00
121777703c
Merge pull request #4557 from tautschnig/__LINE__
...
Regression tests: Ensure __LINE__ is expanded
2019-04-24 13:07:59 +03:00
20861c5a62
Merge pull request #4558 from tautschnig/c-c++-tests
...
Re-use C tests to exercise C++ front-end [blocks: #4558 ]
2019-04-24 13:07:21 +03:00
ff12a5e592
Merge pull request #4564 from tautschnig/fix-ssa-renaming
...
Fix L2 renaming after shift-to-rhs and enable validation
2019-04-24 12:40:24 +03:00
790e455af0
Fix L2 renaming after shift-to-rhs and enable validation
...
When rewriting the RHS to enable field-sensitive LHS-names, we may
introduce the LHS into the RHS, and thus need to re-rename the RHS
expression to ensure all of it is L2. We could have caught this earlier
if we had always enabled SSA validation in regression tests, which is
now done (except for C++ tests, which require a different set of fixes).
2019-04-23 20:27:01 +00:00
01255db77d
avoid access to exprt::opX
...
This avoids out-of-bounds accesses to the operands() vector.
2019-04-23 10:52:05 +01:00
95b110106e
introduce a ranged for
2019-04-23 10:02:19 +01:00
dc67638cfc
avoid access to exprt::opX
...
This prevents out-of-bounds accesses to the operands() vector.
2019-04-23 10:02:19 +01:00
723620dd6c
Re-use C tests to exercise C++ front-end
...
Several C tests should also pass when using the C++ front-end. Use them
to exercise it more and find and fix more bugs. Those that should pass,
but currently don't, are tagged broken-test-c++-front-end.
2019-04-19 22:55:23 +00:00
949b116b10
Ensure __LINE__ is expanded
...
We previously generated several declarations with the same name, because
the C preprocessor does not expand __LINE__ after a concatenation
operator. Add two levels of indirection to achieve this. Using
declarations with the same name was kind of ok for the C front-end, but
is a bug with any C++ front-end.
2019-04-19 17:48:34 +00:00
65e6b6a495
Merge pull request #4547 from danpoe/feature/sharing-map-unit-tests
...
Add unit tests for sharing map that check that views are not invalidated by modifications
2019-04-18 17:51:07 +03:00
620e27deaa
C++ front-end: store typedef names
...
This is already supported in the C front-end, and we should not
unnecessarily deviate in behaviour between the C and C++ front-ends.
2019-04-18 15:05:58 +01:00
44bbea05f4
move goto_functionst::validate into .cpp file
...
The function is large, and thus, this improves compile times.
2019-04-18 15:03:06 +01:00
2b4f0aed2d
Use REQUIRE_THROWS_AS() in sharing map unit tests
2019-04-18 14:37:40 +01:00
2d29291123
Refactor existing tests of error cases to use cbmc_invariants_should_throwt
...
This adds sharing map unit tests to check that operations fail as expected. For
example, calling map.replace(key, value) when the key does not exist in the map
should fail.
2019-04-18 14:37:40 +01:00
94bc97ff31
Add unit tests to check that sharing map modifications do not invalidate views
...
This adds unit tests to check that the references into the sharing map in the
views and delta views remain valid after operations erase(), insert(), and
replace(). The references should remain valid to those elements that are not
changed by the respective operations.
2019-04-18 14:37:40 +01:00
2e7f41473d
Use existing type sharing_map_error_checkt in sharing map unit test
2019-04-18 14:37:40 +01:00
9e348b735c
Fix sharing map unit tests bug that assumed that irep_idts are lexicographically ordered
2019-04-18 14:37:39 +01:00
35c31bbd36
Merge pull request #4533 from diffblue/goto_symex_decision_procedure
...
goto_symex now uses decision_proceduret API
2019-04-18 10:43:48 +03:00
e39318d5de
Merge pull request #4545 from tautschnig/uninitialised-struct-fix
...
Create SSA-level 2 names for individual fields
2019-04-18 09:51:39 +03:00
d535b09561
Merge pull request #4521 from romainbrenguier/clean-up/parse-options-messages
...
Clean-up message_handler of parse_options_baset
2019-04-18 09:48:20 +03:00
49b44074ca
goto symex now uses decision_proceduret interface
...
Use the the decision_proceduret interface in goto_symext instead of
prop_convt. literalt values are replaced by handles.
2019-04-18 07:44:30 +01:00
a5b114e466
switch ssa_stept to handles
...
'Handles' more general than the literalt data structure, which is specific
to propositional, CNF-based SAT.
2019-04-17 22:03:57 +01:00
443ef3c303
models for literal_exprt
...
This enables us to use decision_proceduret::get for handles that are
literal_exprt.
2019-04-17 22:03:57 +01:00
24f4674084
Create SSA-level 2 names for individual fields
...
During symex, a declaration introduces non-deterministic values for the
declared symbol by creating a fresh L2 name without assigning any value
to it. With field-sensitive SSA, the same must be done for each field
(just like we already did the inverse for objects going out of scope via
a DEAD instruction).
2019-04-17 13:41:39 +00:00
262cc351dd
show_goto_functions takes a ui_message_handler
...
This removes the need for passing a seperate ui argument.
2019-04-17 14:37:29 +01:00
747e13b33b
Show properties take a ui_message_handlert
...
This is more precise on the type of message handler we are expecting and
makes the ui argument redundant.
2019-04-17 14:36:57 +01:00
1d09894a7d
Remove unecessary log argument in cbmc_parse_optionst
...
The messaget can be constructed from the message_handler.
2019-04-17 14:36:21 +01:00
Peter Schrammel