diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-25 13:34:13 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-25 13:36:50 +0200 |
| commit | 13bde6f161f2ebe5108023a7e0d3696f2a305719 (patch) | |
| tree | 29f29cf935f88692491e13817000a09b7166e98c /kernel | |
| parent | 915452f9a73d25e45131edb08531c29a79ab7020 (diff) | |
Fix equality check on global names from native compute.
Not sure it could have led to a soundness bug, but this is definitely
serious enough to deserve a backport. Also made the code robust by
listing all the constructors.
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/nativecode.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 6821fc980..74d12f3cd 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -71,6 +71,8 @@ let eq_gname gn1 gn2 = String.equal s1 s2 && eq_constructor c1 c2 | Gconstant (s1, c1), Gconstant (s2, c2) -> String.equal s1 s2 && Constant.equal c1 c2 + | Gproj (s1, ind1, i1), Gproj (s2, ind2, i2) -> + String.equal s1 s2 && eq_ind ind1 ind2 && Int.equal i1 i2 | Gcase (None, i1), Gcase (None, i2) -> Int.equal i1 i2 | Gcase (Some l1, i1), Gcase (Some l2, i2) -> Int.equal i1 i2 && Label.equal l1 l2 | Gpred (None, i1), Gpred (None, i2) -> Int.equal i1 i2 @@ -86,7 +88,9 @@ let eq_gname gn1 gn2 = | Ginternal s1, Ginternal s2 -> String.equal s1 s2 | Grel i1, Grel i2 -> Int.equal i1 i2 | Gnamed id1, Gnamed id2 -> Id.equal id1 id2 - | _ -> false + | (Gind _| Gconstruct _ | Gconstant _ | Gproj _ | Gcase _ | Gpred _ + | Gfixtype _ | Gnorm _ | Gnormtbl _ | Ginternal _ | Grel _ | Gnamed _), _ -> + false let dummy_gname = Grel 0 |