Skip to content
Snippets Groups Projects
Commit 131b3ad9 authored by Julien Signoles's avatar Julien Signoles
Browse files

[E-ACSL] add configure's dependencies

parent 3b0bbdc6
No related branches found
No related tags found
No related merge requests found
...@@ -45,6 +45,9 @@ m4_ifndef([FRAMAC_M4_MACROS], [m4_include(FRAMAC_SHARE/configure.ac)]) ...@@ -45,6 +45,9 @@ m4_ifndef([FRAMAC_M4_MACROS], [m4_include(FRAMAC_SHARE/configure.ac)])
check_plugin(e_acsl,PLUGIN_RELATIVE_PATH(plugin_file), check_plugin(e_acsl,PLUGIN_RELATIVE_PATH(plugin_file),
[support for E-ACSL plug-in],yes,yes) [support for E-ACSL plug-in],yes,yes)
plugin_require(e_acsl,rte_annotation)
check_plugin_dependencies
# Check Frama-C version # Check Frama-C version
####################### #######################
......
...@@ -112,8 +112,7 @@ let meet ty1 ty2 = match ty1, ty2 with ...@@ -112,8 +112,7 @@ let meet ty1 ty2 = match ty1, ty2 with
| (Z | Interv _), No_integral _ | (Z | Interv _), No_integral _
| No_integral _, (Z | Interv _) -> raise Cannot_compare | No_integral _, (Z | Interv _) -> raise Cannot_compare
let join ty1 ty2 = let join ty1 ty2 = match ty1, ty2 with
match ty1, ty2 with
| Interv(l1, u1), Interv(l2, u2) -> Interv(BI.min l1 l2, BI.max u1 u2) | Interv(l1, u1), Interv(l2, u2) -> Interv(BI.min l1 l2, BI.max u1 u2)
| Interv _, Z | Z, Interv _ | Z, Z -> Z | Interv _, Z | Z, Interv _ | Z, Z -> Z
| No_integral t1, No_integral t2 when Logic_type.equal t1 t2 -> ty1 | No_integral t1, No_integral t2 when Logic_type.equal t1 t2 -> ty1
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment