Commit e3cc32aa authored by Andrei Paskevich's avatar Andrei Paskevich

Parser: emit a warning on redundant "import"

parent eae547d9
module M
use import int.Int
use int.Int
type int_type = Integer int
......
......@@ -2,8 +2,8 @@
module Array_records
use import int.Int
use import array.Array
use int.Int
use array.Array
type value = int
type index = int
......
module A
use import int.Int
use import array.Array
use int.Int
use array.Array
let f1 (a:array int) : int
= a[0]
......@@ -16,9 +16,9 @@ end
module B
use import int.Int
use import array.Array
clone import array.Sorted with
use int.Int
use array.Array
clone array.Sorted with
type elt=int,
predicate le=(<=)
......
theory T32
use import ieee_float.Float32
use ieee_float.Float32
goal g1 : forall x:t. eq x (0.0:t)
......@@ -26,7 +26,7 @@ end
theory T64
use import ieee_float.Float64
use ieee_float.Float64
goal g1 : forall x:t. eq x (0.0:t)
......
module Main
use import int.Int
use int.Int
type path_sel_type = { mutable sel_path : bool}
......@@ -12,8 +12,8 @@ end
module Other
use import int.Int
use import Main
use int.Int
use Main
let f (a : int)
ensures {result = 5}
......
theory T
use import int.Int
use int.Int
goal g_lab : forall x [@model] :int. x >= 42 -> x + 3 <= 50
......
module Ce_int32
use import ref.Ref
use ref.Ref
use export mach.int.Int32
let dummy_update (r: ref int32)
......
theory ModelInt
use import int.Int
use int.Int
(* PASS *)
goal test0 : forall x:int. not (0 < x < 1)
......@@ -8,7 +8,7 @@ goal test0 : forall x:int. not (0 < x < 1)
(* CE *)
goal test1 : forall x:int. not (0 <= x <= 1)
use import int.EuclideanDivision
use int.EuclideanDivision
(* CE *)
goal test2 : forall x:int. div x x = 1
......
module M
use import int.Int
use import ref.Ref
use int.Int
use ref.Ref
val a : ref int
......
module Array
use import int.Int
use import array.Array
use int.Int
use array.Array
type t
......
module Abstract
use import int.Int
use int.Int
type byte
function to_int byte : int
......@@ -18,7 +18,7 @@ val add (x y : byte) : byte
requires { [@expl:integer overflow] in_range (to_int x + to_int y) }
ensures { to_int result = to_int x + to_int y }
use import ref.Ref
use ref.Ref
let p3 (a : ref byte) =
a := add !a (of_int 1)
......@@ -27,8 +27,8 @@ end
module Record
use import int.Int
use import Abstract
use int.Int
use Abstract
type r = {mutable f : byte; mutable g : bool}
......
module List_int
use import int.Int
use int.Int
type list = Nil | Cons int list
......@@ -19,8 +19,8 @@ end
module List_poly
use import list.List
use import list.Length
use list.List
use list.Length
goal g1: forall l:list int. length l <> 0
......
theory ModelMap
use import map.Map
use map.Map
goal t1 : forall t:map int int, i : int.
get (set t 0 42) i = get t i
......@@ -9,9 +9,9 @@ end
module M
use import int.Int
use import ref.Ref
use import map.Map
use int.Int
use ref.Ref
use map.Map
let ghost test_map (ghost x : ref (map int int)) : unit
ensures { !x[0] <> !x[1] }
......
theory ModelReal
use import real.Real
use real.Real
goal test1 : forall x:real. not (0.0 < x < 1.0)
......
module M
use import map.Map
use import int.Int
use map.Map
use int.Int
type r = {f [@model_trace:.field_f] :int; g:bool}
......
......@@ -4,8 +4,8 @@
module M
use import ref.Ref
use import int.Int
use ref.Ref
use int.Int
(*** In all cases, records are decomposed using match eval ***)
......@@ -49,7 +49,7 @@ end
module Mutable
use import int.Int
use int.Int
type r = {mutable f [@model_trace:.my_field_f] :int; mutable g:bool}
......
module M
use import ref.Ref
use import list.List
use import int.Int
use ref.Ref
use list.List
use int.Int
let test_post (x: int) (y: ref int): unit
ensures { old !y >= x }
......
module M
use import int.Int
use import ref.Ref
use int.Int
use ref.Ref
val a : ref int
......
theory ModelArray
use import map.Map
use map.Map
goal t1 : forall t: map int int, i: int.
get (set t 0 42) i = get t i
......
module Arith
use import int.Int
use int.Int
goal G1: 0 = 1
use import int.ComputerDivision
use int.ComputerDivision
goal G2: div 1 0 = div 2 0
......
module M
use import int.Int
use import ref.Ref
use int.Int
use ref.Ref
let test (a: (ref int, int))
ensures { let (x, _) = a in !x = (old !x) + 1 }
......
module M
use import int.Int
use import ref.Ref
use int.Int
use ref.Ref
let test1 (x: ref int)
ensures { !x >= old !x }
requires { !x >= 0}
......
......@@ -2,7 +2,7 @@
module Test
use import ref.Refint
use ref.Refint
let test (x: ref int) =
if !x = old !x then 1 else 2
......
module M
use import ref.Ref
use ref.Ref
let foo (x : ref int) (y : ref int) =
x := 1;
......
module M
use import ref.Ref
use ref.Ref
let foo (x : ref int) (y : ref int) =
x := 1;
......
module M
use import ref.Ref
use ref.Ref
let foo (x : ref int) (y : ref int) =
x := 1;
......
module M
use import ref.Ref
use ref.Ref
val r : ref int
......
module M
use import ref.Ref
use ref.Ref
let foo (x : ref int) (y: ref int) =
x := 1;
......
module Bad
use import ref.Ref
use ref.Ref
let f (r: ref int) (x: 'a) : unit
ensures { x = old x /\ !r = 0 }
......
module M
use import ref.Ref
use ref.Ref
val f (x:int) : unit writes {a.contents}
......
module M
use import ref.Ref
use ref.Ref
val f (x:int) : unit writes { x.contents }
......
module M
use import ref.Ref
use ref.Ref
val a : int
......
module M
use import ref.Ref
use ref.Ref
val foo (_x : int) : int
......
module Bad
use import int.Int
use import ref.Ref
use int.Int
use ref.Ref
let f (x y : ref int) : unit
requires { !x = !y }
......
module M
use import ref.Ref
use ref.Ref
(* reference would escape its scope *)
......
module M
use import ref.Ref
use ref.Ref
(* reference would escape its scope *)
......
use import int.Int
use import ref.Ref
use int.Int
use ref.Ref
exception Exit
......
use import int.Int
use import ref.Ref
use int.Int
use ref.Ref
let funny () =
exception FixRegion (ref int) in
......
module M
use import int.Int
use int.Int
let foo () = for i = 1 to () do () done
end
module TestGhost
use import int.Int
use import list.List
use import ref.Ref
use int.Int
use list.List
use ref.Ref
type t = { f1 : int; ghost f2 : (int,list int) }
......
module TestGhost
use import int.Int
use import list.List
use import ref.Ref
use int.Int
use list.List
use ref.Ref
type t = { f1 : int; ghost f2 : int }
......
module Horror
use import ref.Ref
use ref.Ref
let bad (ghost i : int) : ref int
ensures { !result = i }
......
module T
use import ref.Ref
use ref.Ref
let f () =
label Foo in
......
module Bad
use import ref.Ref
use ref.Ref
val function comp 'a 'a : int
......
module Bad
use import ref.Ref
use ref.Ref
val function comp 'a 'a : int
......
module Bad
use import ref.Ref
use ref.Ref
val function comp 'a 'a : ()
......
module M
use import ref.Ref
use ref.Ref
val r : ref 'a
......
module M
use import ref.Ref
use import list.List
use ref.Ref
use list.List
val r : ref (list 'a)
......
module Bad
use import int.Int
use import ref.Ref
use int.Int
use ref.Ref
type dref 'a = { mutable dcontents : ref 'a }
......
module Bad
use import int.Int
use import ref.Ref
use int.Int
use ref.Ref
type dref 'a = { mutable dcontents : ref 'a }
......
module M
use import int.Int
use int.Int
(* missing variant *)
......
......@@ -3,7 +3,7 @@
module M
use import int.Int
use int.Int
predicate rel int int
......
......@@ -3,7 +3,7 @@
module M
use import list.List
use list.List
predicate rel (a b:list 'a)
......
module M
use import int.Int
use int.Int
type t 'a = { a: 'a; b: bool; c: 'a }
......
module M
use import int.Int
use int.Int
type t 'a = { a: 'a; b: bool; c: 'a }
......
use import int.Int
use import ref.Ref
use int.Int
use ref.Ref
val incr (x:ref int) : unit writes {x} ensures { !x = old !x + 1 }
......
exception Exception int
use import ref.Ref
use ref.Ref
val t : ref int
......
module M
use import int.Int
use import ref.Ref
use int.Int
use ref.Ref
exception Break
......
......@@ -39,8 +39,8 @@ let p6 () ensures { false } raises { E -> true | F _ -> false }
(* composition of exceptions with side-effect on a reference *)
use import int.Int
use import ref.Ref
use int.Int
use ref.Ref
val x : ref int
......
module M
use import int.Int
use import ref.Ref
use int.Int
use ref.Ref
(* for loop with invariant *)
let test1 () =
......
module Labels
use import int.Int
use import ref.Ref
use int.Int
use ref.Ref
function fst (x: ('a, 'b)) : 'a = let (x1, _) = x in x1
......
module M
use import int.Int
use import list.List
use import list.Length
use int.Int
use list.List
use list.Length
let rec append (l1 : list 'a) (l2 : list 'a) variant { length l1 }
ensures { length result = length l1 + length l2 }
......
module M
use import int.Int
use import ref.Ref
use int.Int
use ref.Ref
(** 1. A loop increasing [i] up to 10. *)
......
module M
use import int.Int
use import int.EuclideanDivision
use int.Int
use int.EuclideanDivision
predicate even (x : int) = x = 2 * (div x 2)
predicate odd (x : int) = x = 2 * (div x 2) + 1
......
module T
use import int.Int
use int.Int
exception MyExc
......
module M
use import ref.Ref
use ref.Ref