Skip to content
Snippets Groups Projects
Commit e7c5bea4 authored by Loïc Correnson's avatar Loïc Correnson
Browse files

Merge branch 'bugfix/wp-qed-smp_cmp_with_lsr' into 'stable/calcium'

[WP/QED] Fixes comparison with lsr

See merge request frama-c/frama-c!2450
parents 22bc078f 18c61560
No related branches found
No related tags found
No related merge requests found
...@@ -721,7 +721,7 @@ let smp_cmp_with_lsr cmp a0 b0 = ...@@ -721,7 +721,7 @@ let smp_cmp_with_lsr cmp a0 b0 =
e/A2 cmp b2 <==> (e/A2)*A2 cmp b2*A2) with A2==2**a2 e/A2 cmp b2 <==> (e/A2)*A2 cmp b2*A2) with A2==2**a2
So, A2>0 and (e/A2)*A2 == e&~((2**a2)-1) So, A2>0 and (e/A2)*A2 == e&~((2**a2)-1)
*) *)
mk_cmp_with_lsr_cst e_eq e a2 b1 mk_cmp_with_lsr_cst cmp e a2 b1
with Not_found -> with Not_found ->
(* This rule takes into acount several cases. (* This rule takes into acount several cases.
One of them is One of them is
......
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