Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
F
FloVer
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
5
Issues
5
List
Boards
Labels
Service Desk
Milestones
Operations
Operations
Incidents
Analytics
Analytics
Repository
Value Stream
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Commits
Issue Boards
Open sidebar
AVA
FloVer
Commits
dee127fa
Commit
dee127fa
authored
Mar 12, 2018
by
Heiko Becker
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Fix type renaming also for regression tests
parent
43aa5724
Changes
3
Hide whitespace changes
Inline
Side-by-side
Showing
3 changed files
with
31 additions
and
31 deletions
+31
-31
testcases/regression/certificate_AdditionSimple.v
testcases/regression/certificate_AdditionSimple.v
+3
-3
testcases/regression/certificate_Doppler.v
testcases/regression/certificate_Doppler.v
+13
-13
testcases/regression/certificate_HimmilbeauLet.v
testcases/regression/certificate_HimmilbeauLet.v
+15
-15
No files found.
testcases/regression/certificate_AdditionSimple.v
View file @
dee127fa
Require
Import
Flover
.
CertificateChecker
.
Definition
C12
:
exp
Q
:=
Const
M64
((
1657
)#(
5
)).
Definition
u0
:
exp
Q
:=
Var
Q
0.
Definition
e3
:
exp
Q
:=
Binop
Plus
C12
u0
.
Definition
C12
:
exp
r
Q
:=
Const
M64
((
1657
)#(
5
)).
Definition
u0
:
exp
r
Q
:=
Var
Q
0.
Definition
e3
:
exp
r
Q
:=
Binop
Plus
C12
u0
.
Definition
Rete3
:=
Ret
e3
.
...
...
testcases/regression/certificate_Doppler.v
View file @
dee127fa
Require
Import
Flover
.
CertificateChecker
.
Definition
C12
:
exp
Q
:=
Const
M64
((
1657
)#(
5
)).
Definition
C34
:
exp
Q
:=
Const
M64
((
3
)#(
5
)).
Definition
T2
:
exp
Q
:=
Var
Q
2.
Definition
e5
:
exp
Q
:=
Binop
Mult
C34
T2
.
Definition
e6
:
exp
Q
:=
Binop
Plus
C12
e5
.
Definition
t15
:
exp
Q
:=
Var
Q
5.
Definition
UMint15
:
exp
Q
:=
Unop
Neg
t15
.
Definition
v1
:
exp
Q
:=
Var
Q
1.
Definition
e7
:
exp
Q
:=
Binop
Mult
UMint15
v1
.
Definition
u0
:
exp
Q
:=
Var
Q
0.
Definition
e8
:
exp
Q
:=
Binop
Plus
t15
u0
.
Definition
e9
:
exp
Q
:=
Binop
Mult
e8
e8
.
Definition
e10
:
exp
Q
:=
Binop
Div
e7
e9
.
Definition
C12
:
exp
r
Q
:=
Const
M64
((
1657
)#(
5
)).
Definition
C34
:
exp
r
Q
:=
Const
M64
((
3
)#(
5
)).
Definition
T2
:
exp
r
Q
:=
Var
Q
2.
Definition
e5
:
exp
r
Q
:=
Binop
Mult
C34
T2
.
Definition
e6
:
exp
r
Q
:=
Binop
Plus
C12
e5
.
Definition
t15
:
exp
r
Q
:=
Var
Q
5.
Definition
UMint15
:
exp
r
Q
:=
Unop
Neg
t15
.
Definition
v1
:
exp
r
Q
:=
Var
Q
1.
Definition
e7
:
exp
r
Q
:=
Binop
Mult
UMint15
v1
.
Definition
u0
:
exp
r
Q
:=
Var
Q
0.
Definition
e8
:
exp
r
Q
:=
Binop
Plus
t15
u0
.
Definition
e9
:
exp
r
Q
:=
Binop
Mult
e8
e8
.
Definition
e10
:
exp
r
Q
:=
Binop
Div
e7
e9
.
Definition
Rete10
:=
Ret
e10
.
Definition
Lett15e6Rete10
:=
Let
M64
5
e6
Rete10
.
...
...
testcases/regression/certificate_HimmilbeauLet.v
View file @
dee127fa
Require
Import
Flover
.
CertificateChecker
.
Definition
x10
:
exp
Q
:=
Var
Q
0.
Definition
e1
:
exp
Q
:=
Binop
Mult
x10
x10
.
Definition
x21
:
exp
Q
:=
Var
Q
1.
Definition
e2
:
exp
Q
:=
Binop
Plus
e1
x21
.
Definition
t14
:
exp
Q
:=
Var
Q
4.
Definition
e3
:
exp
Q
:=
Binop
Mult
x21
x21
.
Definition
e4
:
exp
Q
:=
Binop
Plus
x10
e3
.
Definition
t25
:
exp
Q
:=
Var
Q
5.
Definition
C56
:
exp
Q
:=
Const
M64
((
11
)#(
1
)).
Definition
e7
:
exp
Q
:=
Binop
Sub
t14
C56
.
Definition
e8
:
exp
Q
:=
Binop
Mult
e7
e7
.
Definition
C910
:
exp
Q
:=
Const
M64
((
7
)#(
1
)).
Definition
e11
:
exp
Q
:=
Binop
Sub
t25
C910
.
Definition
e12
:
exp
Q
:=
Binop
Mult
e11
e11
.
Definition
e13
:
exp
Q
:=
Binop
Plus
e8
e12
.
Definition
x10
:
exp
r
Q
:=
Var
Q
0.
Definition
e1
:
exp
r
Q
:=
Binop
Mult
x10
x10
.
Definition
x21
:
exp
r
Q
:=
Var
Q
1.
Definition
e2
:
exp
r
Q
:=
Binop
Plus
e1
x21
.
Definition
t14
:
exp
r
Q
:=
Var
Q
4.
Definition
e3
:
exp
r
Q
:=
Binop
Mult
x21
x21
.
Definition
e4
:
exp
r
Q
:=
Binop
Plus
x10
e3
.
Definition
t25
:
exp
r
Q
:=
Var
Q
5.
Definition
C56
:
exp
r
Q
:=
Const
M64
((
11
)#(
1
)).
Definition
e7
:
exp
r
Q
:=
Binop
Sub
t14
C56
.
Definition
e8
:
exp
r
Q
:=
Binop
Mult
e7
e7
.
Definition
C910
:
exp
r
Q
:=
Const
M64
((
7
)#(
1
)).
Definition
e11
:
exp
r
Q
:=
Binop
Sub
t25
C910
.
Definition
e12
:
exp
r
Q
:=
Binop
Mult
e11
e11
.
Definition
e13
:
exp
r
Q
:=
Binop
Plus
e8
e12
.
Definition
Rete13
:=
Ret
e13
.
Definition
Lett25e4Rete13
:=
Let
M64
5
e4
Rete13
.
Definition
Lett14e2Lett25e4Rete13
:=
Let
M64
4
e2
Lett25e4Rete13
.
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment