Merge branch 'fix/acsl/polymorphic-inductive' into 'master'

[ACSL] Type var of polymorphic inductives are not in scope in cases anymore

See merge request frama-c/frama-c!4143

src/kernel_internals/parsing/logic_parser.mly

@@ -1657,10 +1657,11 @@ logic_def:
       exit_type_variables_scope ();
       LDpredicate_def (id, labels, tvars, $3, $5) }
 /* inductive predicate definition */
-| INDUCTIVE poly_id parameters LBRACE indcases RBRACE
-    { let (id,labels,tvars) = $2 in
-      exit_type_variables_scope ();
-      LDinductive_def(id, labels, tvars, $3, $5) }
+| INDUCTIVE pred = poly_id params = parameters
+    midrule({exit_type_variables_scope()})
+    LBRACE cases = indcases RBRACE
+    { let (id,labels,tvars) = pred in
+      LDinductive_def(id, labels, tvars, params, cases) }
 | LEMMA poly_id COLON lexpr SEMICOLON
     { let (id,labels,tvars) = $2 in
       exit_type_variables_scope ();

tests/spec/oracle/polymorphic_inductive.res.oracle

+[kernel] Parsing polymorphic_inductive.i (no preprocessing)
+/* Generated by Frama-C */
+/*@
+inductive P<A>(A i, \list<A>  s) {
+  case one<A>: ∀ A a, \list<A>  s; \Cons(a, s) ≡ [| a |] ⇒ P(a, s);
+  }
+ */
+

tests/spec/polymorphic_inductive.i

+/*@ inductive P<A>(A i, \list<A> s){
+    case one<A>: 
+      \forall A a, \list<A> s ; \Cons(a, s) == [| a |] ==> P(a, s);
+    }
+*/