Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

Commit 91b9f5bc authored by Andrei Paskevich's avatar Andrei Paskevich

Parser: drop syntax "abstract <spec> <expr_seq> end"

use "begin <spec> <expr_seq> end" instead. The word "abstract" is
now only used to declare a private type whose fields are all ghost.
parent b9d879d9
......@@ -706,7 +706,7 @@ module Map
(forall k2:K.t. CO.lt k k2 -> rg.m.func k2 = t.m.func k2) /\
(forall k2:K.t. CO.le k2 k -> rg.m.func k2 = None) }
= let (lf,o,rg) = MB.split k t in
let o = abstract ensures { match o with None -> result = None
let o = begin ensures { match o with None -> result = None
| Some (_,v) -> result = Some v end }
match o with None -> None | Some (_,v) -> Some v end end in
(lf,o,rg)
......@@ -896,7 +896,7 @@ module Set
(forall k2. CO.le k k2 -> not lf.m.set k2) /\
(forall k2. CO.le k2 k -> not rg.m.set k2) }
= let (lf,o,rg) = MB.split k t in
let o = abstract ensures { result <-> o <> None }
let o = begin ensures { result <-> o <> None }
match o with None -> false | _ -> true end end in
(lf,o,rg)
......
......@@ -48,7 +48,7 @@ module Bitwalker
ensures { flag = BV64.nth result (63 - BV32.to_uint left) }
=
assert { BV32.ult left (BV32.of_int 64) };
abstract
begin
ensures { forall i:BV32.t. i <> BV32.sub (BV32.of_int 63) left ->
BV64.nth_bv result (C32_64.toBig i) =
BV64.nth_bv value (C32_64.toBig i) }
......@@ -77,7 +77,7 @@ module Bitwalker
let ghost left_bv = BV64.of_int left in
assert { BV64.ult left_bv (BV64.of_int 64) };
assert { (BV64.sub (BV64.of_int 63) left_bv) = BV64.of_int (63 - left) };
abstract
begin
ensures { forall i:BV64.t. BV64.ule i (BV64.of_int 63) ->
i <> BV64.sub (BV64.of_int 63) left_bv ->
BV64.nth_bv result i = BV64.nth_bv value i }
......@@ -100,7 +100,7 @@ module Bitwalker
ensures { result = BV8.nth byte (7 - BV32.to_uint left) }
=
assert {BV32.ult left (BV32.of_int 8)};
abstract
begin
ensures {
result = BV8.nth_bv
byte (BV8.sub (BV8.of_int 7) (C8_32.toSmall left))}
......@@ -168,7 +168,7 @@ module Bitwalker
ensures {result = BV64.nth value (63 - BV32.to_uint left)}
=
assert {BV32.ult left (BV32.of_int 64)};
abstract
begin
ensures {result = BV64.nth_bv value
(BV64.sub (BV64.of_int 63) (C32_64.toBig left))}
let mask = BV64.lsl_bv (BV64.int_check 1)
......@@ -193,7 +193,7 @@ module Bitwalker
ensures { BV8.nth result (7 - BV32.to_uint left) = flag }
=
assert { BV32.ult left (BV32.of_int 8) };
abstract
begin
ensures { forall i:BV32.t. BV32.ult i (BV32.of_int 8) ->
i <> BV32.sub (BV32.of_int 7) left ->
BV8.nth_bv result (C8_32.toSmall i)
......
......@@ -150,7 +150,7 @@ module HashtblImpl
ensures { forall k': key. k' <> k ->
Map.get h.view k' = Map.get (old h.view) k' }
=
abstract if h.size = length h.data then resize h end;
if h.size = length h.data then resize h;
remove h k;
let i = bucket k (length h.data) in
h.data[i] <- Cons (k, v) h.data[i];
......
......@@ -207,7 +207,7 @@ module LinearProbing
writes { h.size, h.data, h.data.elts, h.view, h.loc }
ensures { h.view = Map.set (old h.view) (keym x) True }
=
abstract
begin
ensures { h.size + 1 < Array.length h.data }
if 2 * (h.size + 1) >= Array.length h.data then resize h
end;
......
......@@ -28,7 +28,7 @@ syn match whyBraceErr "}"
syn match whyBrackErr "\]"
syn match whyParenErr ")"
syn match whyCommentErr "\(^\|[^(]\)\*)"
syn match whyCommentErr "\*)"
syn match whyCountErr "\<downto\>"
syn match whyCountErr "\<to\>"
......@@ -52,13 +52,14 @@ syn region whyEncl transparent matchgroup=whyKeyword start="{" matchgroup=whyK
syn region whyEncl transparent matchgroup=whyKeyword start="\[" matchgroup=whyKeyword end="\]" contains=ALLBUT,@whyContained,whyBrackErr
" Comments
syn region whyComment start="(\*\([^)]\|$\)" end="\(^\|[^(]\)\*)" contains=whyComment,whyTodo
syn region whyComment start="(\*" end="\*)" contains=whyComment,whyTodo
syn match whyOperator "(\*)"
syn keyword whyTodo contained TODO FIXME XXX NOTE
" Blocks
" FIXME? match and try should detect the absence of "with" ?
syn region whyEnd matchgroup=whyKeyword start="\<begin\>" matchgroup=whyKeyword end="\<end\>" contains=ALLBUT,@whyContained,whyEndErr
syn region whyEnd matchgroup=whyKeyword start="\<abstract\>" matchgroup=whyKeyword end="\<end\>" contains=ALLBUT,@whyContained,whyEndErr
syn region whyEnd matchgroup=whyKeyword start="\<match\>" matchgroup=whyKeyword end="\<end\>" contains=ALLBUT,@whyContained,whyEndErr
syn region whyEnd matchgroup=whyKeyword start="\<loop\>" matchgroup=whyKeyword end="\<end\>" contains=ALLBUT,@whyContained,whyEndErr
syn region whyEnd matchgroup=whyKeyword start="\<try\>" matchgroup=whyKeyword end="\<end\>" contains=ALLBUT,@whyContained,whyEndErr
......@@ -68,18 +69,15 @@ syn region whyNone matchgroup=whyKeyword start="\<if\>" matchgroup=whyKeyword
" Theories and modules
syn region whyTheory matchgroup=whyKeyword start="\<theory\>" matchgroup=whyModSpec end="\<\u\(\w\|'\)*\>" contains=@whyAllErrs,whyComment skipwhite skipempty nextgroup=whyTheoryContents
syn region whyTheory matchgroup=whyKeyword start="\<theory\>" matchgroup=whyModSpec end="\<\u\(\w\|'\)*\>" contains=@whyAllErrs,whyComment skipwhite skipempty nextgroup=whyModuleContents
syn region whyModule matchgroup=whyKeyword start="\<module\>" matchgroup=whyModSpec end="\<\u\(\w\|'\)*\>" contains=@whyAllErrs,whyComment skipwhite skipempty nextgroup=whyModuleContents
syn region whyScope matchgroup=whyKeyword start="\<scope\>" matchgroup=whyModSpec end="\<\u\(\w\|'\)*\>" contains=@whyAllErrs,whyComment,whyImport skipwhite skipempty nextgroup=whyScopeContents
syn region whyScope matchgroup=whyKeyword start="\<scope\>" matchgroup=whyModSpec end="\<\u\(\w\|'\)*\>" contains=@whyAllErrs,whyComment,whyImport skipwhite skipempty nextgroup=whyModuleContents
syn region whyTheoryContents start="^" start="."me=e-1 matchgroup=whyModSpec end="\<end\>" contained contains=ALLBUT,@whyContained,whyEndErr,whyTheory,whyModule
syn region whyModuleContents start="^" start="."me=e-1 matchgroup=whyModSpec end="\<end\>" contained contains=ALLBUT,@whyContained,whyEndErr,whyTheory,whyModule
syn region whyScopeContents start="^" start="."me=e-1 matchgroup=whyModSpec end="\<end\>" contained contains=ALLBUT,@whyContained,whyEndErr,whyTheory,whyModule
syn region whyModuleContents start="" matchgroup=whyModSpec end="\<end\>" contained contains=ALLBUT,@whyContained,whyEndErr,whyTheory,whyModule
syn region whyNone matchgroup=whyKeyword start="\<\(use\|clone\)\>" matchgroup=whyModSpec end="\<\(\w\+\.\)*\u\(\w\|'\)*\>" contains=@whyAllErrs,whyComment,whyString,whyImport,whyExport,whyModuleKeyword
syn region whyNone matchgroup=whyKeyword start="\<\(use\|clone\)\>" matchgroup=whyModSpec end="\<\(\w\+\.\)*\u\(\w\|'\)*\>" contains=@whyAllErrs,whyComment,whyString,whyImport,whyExport
syn keyword whyExport contained export
syn keyword whyImport contained import
syn keyword whyModuleKeyword contained module
syn region whyNone matchgroup=whyKeyword start="\<\(axiom\|lemma\|goal\)\>" matchgroup=whyNone end="\<\w\(\w\|'\)*\>" contains=@whyAllErrs,whyComment
......@@ -91,7 +89,7 @@ syn keyword whyKeyword let meta
syn keyword whyKeyword not predicate so
syn keyword whyKeyword then type with
syn keyword whyKeyword any
syn keyword whyKeyword abstract any
syn keyword whyKeyword exception fun ghost label
syn keyword whyKeyword model mutable private
syn keyword whyKeyword raise rec val while
......@@ -140,7 +138,7 @@ syn sync maxlines=500
syn sync match whyDoSync grouphere whyDo "\<do\>"
syn sync match whyDoSync groupthere whyDo "\<done\>"
syn sync match whyEndSync grouphere whyEnd "\<\(begin\|abstract\|match\|loop\|try\)\>"
syn sync match whyEndSync grouphere whyEnd "\<\(begin\|match\|loop\|try\)\>"
syn sync match whyEndSync groupthere whyEnd "\<end\>"
syn sync match whyTheorySync grouphere whyTheory "\<theory\>"
......
......@@ -763,8 +763,6 @@ expr_:
{ Erec ($3, $5) }
| FUN binders spec ARROW spec seq_expr
{ Efun ($2, None, Ity.MaskVisible, spec_union $3 $5, $6) }
| ABSTRACT spec seq_expr END
{ Efun ([], None, Ity.MaskVisible, $2, $3) }
| ANY return spec
{ Eany ([], Expr.RKnone, Some (fst $2), snd $2, $3) }
| VAL ghost kind labels(lident_rich) mk_expr(val_defn) IN seq_expr
......@@ -813,7 +811,11 @@ expr_dot_:
| expr_sub { $1 }
expr_sub:
| expr_dot DOT lqualid_rich { Eidapp ($3, [$1]) }
| BEGIN single_spec spec seq_expr END
{ Efun ([], None, Ity.MaskVisible, spec_union $2 $3, $4) }
| BEGIN single_spec spec END
{ let e = mk_expr (Etuple []) $startpos $endpos in
Efun ([], None, Ity.MaskVisible, spec_union $2 $3, e) }
| BEGIN seq_expr END { $2.expr_desc }
| LEFTPAR seq_expr RIGHTPAR { $2.expr_desc }
| BEGIN END { Etuple [] }
......@@ -821,6 +823,7 @@ expr_sub:
| LEFTPAR comma_list2(expr) RIGHTPAR { Etuple $2 }
| LEFTBRC field_list1(expr) RIGHTBRC { Erecord $2 }
| LEFTBRC expr_arg WITH field_list1(expr) RIGHTBRC { Eupdate ($2, $4) }
| expr_dot DOT lqualid_rich { Eidapp ($3, [$1]) }
| expr_arg LEFTSQ expr RIGHTSQ
{ Eidapp (get_op $startpos($2) $endpos($2), [$1;$3]) }
| expr_arg LEFTSQ expr LARROW expr RIGHTSQ
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment