- Oct 02, 2023
-
-
-
-
Allan Blanchard authored
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
- Hashtbl stores a bool to remember if bhv has assumes clauses - When looking for clauses to combine for default behavior, we search in that order (and stop if we found some clauses) : - unguarded behaviors (no assumes). - complete behaviors (each one of them needs to be in our table). - all behaviors in our table. It is a generic function used by {!Generator.get_clauses}.
-
-
-
-
- Only generates assigns clauses when required: - when the analysis uses the specification to analyze a function (decided in function_calls.ml) - for Frama_C_* builtins, such as Frama_C_assert. Others builtins should already have a specification. - when interpreting a Frama_C_show_each directive, so other plugins known these functions have no effect. - in [Logic_inout.valid_behaviors], used by inout and from plugins to interpret a function specification. - Also generates assigns clauses for functions with a body: this is required for the analysis of recursive functions and of functions specified in the -eva-use-spec parameter (in both case, a specific Eva warning is emitted). - In recursion.ml, renames get_spec to check_spec. The generation of assigns clauses is now uniformly done in function_calls.
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-