Change member_shift (fix rems-project/cerberus#728)

This commit propagates a breaking change to syntax of CN, specifically
member_shift

Previously:
```c
struct s;
typedef struct s td;
/*@ member_shift<s>(..); @*/  // <-- okay
/*@ member_shift<struct s>(..); @*/ // <-- not allowed
/*@ member_shift<td>(..); @*/ // <-- not supported
```

Now:
```c
struct s;
typedef struct s td;
/*@ member_shift<s>(..); @*/  // <-- not allowed
/*@ member_shift<struct s>(..); @*/ // <-- okay
/*@ member_shift<td>(..); @*/ // <-- okay
```

The change is breaking, and it's seems impractical to do it in a
backwards compatible way because of a parser conflict, but is easy to
update with a simple sed command `sed -i 's/member_shift</&struct /g'`.

Author: dc-mak

cn.opam

@@ -23,7 +23,7 @@ depends: [
   "zarith" {>= "1.13"}
 ]
 pin-depends: [
-  ["cerberus-lib.dev" "git+https://github.com/rems-project/cerberus.git#3c75d1b"]
+  ["cerberus-lib.dev" "git+https://github.com/rems-project/cerberus.git#2d84326"]
 ]
 build: [
   ["dune" "subst"] {pinned}

lib/compile.ml

@@ -882,7 +882,7 @@ module EffectfulTranslation = struct
           return (IT (it_, Loc (Some member_ty), loc))
         in
         (match (opt_tag, IT.get_bt e) with
-         | Some tag, Loc (Some (Struct tag')) ->
+         | Some (Ctype (_, Struct tag)), Loc (Some (Struct tag')) ->
            if Sym.equal tag tag' then
              with_tag tag
            else (
@@ -895,7 +895,8 @@ module EffectfulTranslation = struct
                      (Illtyped_it
                         { it = Terms.pp e; has = SBT.pp (Struct tag'); expected; reason })
                })
-         | Some tag, Loc None | None, Loc (Some (Struct tag)) -> with_tag tag
+         | Some (Ctype (_, Struct tag)), Loc None | None, Loc (Some (Struct tag)) ->
+           with_tag tag
          | None, Loc None -> cannot_tell_pointee_ctype loc e
          | _, has ->
            let expected = "struct pointer" in

lib/pp_mucore_coq.ml

@@ -1548,7 +1548,7 @@ let rec pp_cn_expr ppfa ppfty = function
                  "CNExpr_membershift"
                  [ pp_triple
                      (pp_cn_expr ppfa ppfty)
-                     (pp_option ppfa)
+                     (pp_option ppfty)
                      pp_identifier
                      (e, oa, id)
                  ]

tests/cn/has_alloc_id_shift.c

@@ -28,7 +28,7 @@ struct s {
 void member_shift(struct s *p)
 /*@
 requires
-    has_alloc_id(member_shift<s>(p, x));
+    has_alloc_id(member_shift<struct s>(p, x));
 ensures
     has_alloc_id(p);
 @*/

tests/cn/list_literal_type.error.c.verify

@@ -1,5 +1,5 @@
 return code: 2
 tests/cn/list_literal_type.error.c:3:15: error: unexpected token after 'list' and before '<'
-Please add error message for state 1889 to parsers/c/c_parser_error.messages
+Please add error message for state 1842 to parsers/c/c_parser_error.messages
 function (list<integer>) nonempty_list() {
               ^ 

tests/cn/tree16/as_mutual_dt/tree16.c

@@ -38,7 +38,7 @@ predicate {datatype tree t, i32 v, map <i32, datatype tree> children}
   else {
     take P = RW<struct node>(p);
     let V = P.v;
-    let nodes_ptr = member_shift<node>(p,nodes);
+    let nodes_ptr = member_shift<struct node>(p,nodes);
     take Ns = each (i32 i; (0i32 <= i) && (i < NUM_NODES))
       {Indirect_Tree(array_shift<tree>(nodes_ptr, i))};
     let ts = array_to_tree_list (Ns, NUM_NODES);

tests/cn/tree16/as_mutual_dt/tree16.c.verify

@@ -11,8 +11,8 @@ tests/cn/tree16/as_mutual_dt/tree16.c:111:19: warning: 'each' prefers a 'u64', b
 tests/cn/tree16/as_mutual_dt/tree16.c:121:18: warning: 'each' prefers a 'u64', but 'j' has type 'i32'.
             take Xs2 = each (i32 j; (0i32 <= j) && (j < path_len))
                  ^
-other location (File "lib/compile.ml", line 1630, characters 38-45)  warning: 'focus' prefers a 'u64', but 'read_&i1' has type 'i32'.
+other location (File "lib/compile.ml", line 1631, characters 38-45)  warning: 'focus' prefers a 'u64', but 'read_&i1' has type 'i32'.
 
-other location (File "lib/compile.ml", line 1630, characters 38-45)  warning: 'focus' prefers a 'u64', but 'read_&idx0' has type 'i32'.
+other location (File "lib/compile.ml", line 1631, characters 38-45)  warning: 'focus' prefers a 'u64', but 'read_&idx0' has type 'i32'.
 
 [1/1]: lookup_rec -- pass

tests/cn/tree16/as_partial_map/tree16.c

@@ -51,7 +51,7 @@ predicate {map<datatype tree_arc, datatype tree_node_option> t,
   else {
     take P = RW<struct node>(p);
     let V = P.v;
-    let nodes_ptr = member_shift<node>(p,nodes);
+    let nodes_ptr = member_shift<struct node>(p,nodes);
     take Ns = each (i32 i; (0i32 <= i) && (i < (num_nodes ())))
       {Indirect_Tree(array_shift<tree>(nodes_ptr, i))};
     let t = construct (V, Ns);

tests/cn/tree16/as_partial_map/tree16.c.verify

@@ -17,9 +17,9 @@ tests/cn/tree16/as_partial_map/tree16.c:137:19: warning: 'each' prefers a 'u64',
 tests/cn/tree16/as_partial_map/tree16.c:146:18: warning: 'each' prefers a 'u64', but 'j' has type 'i32'.
             take Xs2 = each (i32 j; (0i32 <= j) && (j < path_len))
                  ^
-other location (File "lib/compile.ml", line 1630, characters 38-45)  warning: 'focus' prefers a 'u64', but 'read_&i2' has type 'i32'.
+other location (File "lib/compile.ml", line 1631, characters 38-45)  warning: 'focus' prefers a 'u64', but 'read_&i2' has type 'i32'.
 
-other location (File "lib/compile.ml", line 1630, characters 38-45)  warning: 'focus' prefers a 'u64', but 'read_&idx0' has type 'i32'.
+other location (File "lib/compile.ml", line 1631, characters 38-45)  warning: 'focus' prefers a 'u64', but 'read_&idx0' has type 'i32'.
 
 [1/2]: cn_get_num_nodes -- pass
 [2/2]: lookup_rec -- pass