Skip to content

update following [] rewrite move downstream pog [#81070] #7

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
dde-cls merged 1 commit into from
Apr 17, 2026
Merged

update following [] rewrite move downstream pog [#81070] #7

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion extern/BAST
Open in desktop
Submodule BAST updated 6 files
+13 −0 src/expr.cpp
+4 −0 src/expr.h
+4 −0 src/exprPrinter.cpp
+4 −1 src/exprReader.cpp
+6 −0 src/exprWriter.cpp
+1 −1 src/pred.cpp
1 change: 1 addition & 0 deletions test/CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,3 +18,4 @@ macro(add_pog_test id)
endmacro(add_pog_test)

# add_pog_test(empty_1)
# add_pog_test(emptyseq_1)
8 changes: 8 additions & 0 deletions test/input/emptyseq_1/emptyseq_1.mch
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
MACHINE emptyseq_1
ABSTRACT_CONSTANTS
empty_seq
PROPERTIES
empty_seq : seq(INTEGER )
ASSERTIONS
empty_seq = []
END
88 changes: 88 additions & 0 deletions test/input/emptyseq_1/input.pog
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,88 @@
<?xml version="1.0" encoding="UTF-8"?>
<Proof_Obligations xmlns="https://www.atelierb.eu/Formats/pog" version="1.0">
<Define name="B definitions" hash="7128875304803749033">
<Exp_Comparison op="=">
<Id value="NAT" typref="0"/>
<Binary_Exp op=".." typref="0">
<Integer_Literal value="0" typref="1"/>
<Id value="MAXINT" typref="1"/>
</Binary_Exp>
</Exp_Comparison>
<Exp_Comparison op="=">
<Id value="INT" typref="0"/>
<Binary_Exp op=".." typref="0">
<Id value="MININT" typref="1"/>
<Id value="MAXINT" typref="1"/>
</Binary_Exp>
</Exp_Comparison>
</Define>
<Define name="ctx" hash="0"/>
<Define name="seext" hash="0"/>
<Define name="lprp" hash="13959555193171451369">
<Exp_Comparison op=":">
<Id value="empty_seq" typref="2" tag="emptyseq_1.bxml:1:2:1:1"/>
<Unary_Exp op="seq" typref="3">
<Id value="INTEGER" typref="0" tag="emptyseq_1.bxml:1:2:1:2:1"/>
</Unary_Exp>
</Exp_Comparison>
</Define>
<Define name="inprp" hash="0"/>
<Define name="inext" hash="0"/>
<Define name="inv" hash="0"/>
<Define name="ass" hash="9854762428728149081">
<Exp_Comparison op="=">
<Id value="empty_seq" typref="2" tag="emptyseq_1.bxml:1:4:1:1"/>
<EmptySeq typref="2" tag="emptyseq_1.bxml:1:4:1:2"/>
</Exp_Comparison>
</Define>
<Define name="cst" hash="0"/>
<Define name="sets" hash="0"/>
<Proof_Obligation goalHash="9854763489016687786">
<Tag>AssertionLemmas</Tag>
<Definition name="B definitions"/>
<Definition name="ctx"/>
<Definition name="cst"/>
<Definition name="lprp"/>
<Definition name="inprp"/>
<Definition name="inext"/>
<Definition name="seext"/>
<Definition name="inv"/>
<Simple_Goal>
<Tag>Assertion is verified</Tag>
<Goal>
<Exp_Comparison op="=">
<Id value="empty_seq" typref="2" tag="emptyseq_1.bxml:1:4:1:1"/>
<EmptySeq typref="2" tag="emptyseq_1.bxml:1:4:1:2"/>
</Exp_Comparison>
</Goal>
</Simple_Goal>
</Proof_Obligation>
<TypeInfos>
<Type id="0">
<Unary_Exp op="POW">
<Id value="INTEGER"/>
</Unary_Exp>
</Type>
<Type id="1">
<Id value="INTEGER"/>
</Type>
<Type id="2">
<Unary_Exp op="POW">
<Binary_Exp op="*">
<Id value="INTEGER"/>
<Id value="INTEGER"/>
</Binary_Exp>
</Unary_Exp>
</Type>
<Type id="3">
<Unary_Exp op="POW">
<Unary_Exp op="POW">
<Binary_Exp op="*">
<Id value="INTEGER"/>
<Id value="INTEGER"/>
</Binary_Exp>
</Unary_Exp>
</Unary_Exp>
</Type>
</TypeInfos>
</Proof_Obligations>
1 change: 1 addition & 0 deletions test/output/reference/emptyseq_1/exitcode
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
0
87 changes: 87 additions & 0 deletions test/output/reference/emptyseq_1/output.pog
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,87 @@
<Proof_Obligations>
<Define name="B definitions" hash="7128875304803749033">
<Exp_Comparison op="=">
<Id value="NAT" typref="0"/>
<Binary_Exp op=".." typref="0">
<Integer_Literal value="0" typref="1"/>
<Id value="MAXINT" typref="1"/>
</Binary_Exp>
</Exp_Comparison>
<Exp_Comparison op="=">
<Id value="INT" typref="0"/>
<Binary_Exp op=".." typref="0">
<Id value="MININT" typref="1"/>
<Id value="MAXINT" typref="1"/>
</Binary_Exp>
</Exp_Comparison>
</Define>
<Define name="ctx"/>
<Define name="seext"/>
<Define name="lprp" hash="13959555193171451369">
<Exp_Comparison op=":">
<Id value="empty_seq" typref="2" tag="emptyseq_1.bxml:1:2:1:1"/>
<Unary_Exp op="seq" typref="3">
<Id value="INTEGER" typref="0" tag="emptyseq_1.bxml:1:2:1:2:1"/>
</Unary_Exp>
</Exp_Comparison>
</Define>
<Define name="inprp"/>
<Define name="inext"/>
<Define name="inv"/>
<Define name="ass" hash="9854762428728149081">
<Exp_Comparison op="=">
<Id value="empty_seq" typref="2" tag="emptyseq_1.bxml:1:4:1:1"/>
<EmptySeq typref="2" tag="emptyseq_1.bxml:1:4:1:2"/>
</Exp_Comparison>
</Define>
<Define name="cst"/>
<Define name="sets"/>
<Proof_Obligation goalHash="9854763489016687786">
<Tag>AssertionLemmas</Tag>
<Definition name="B definitions"/>
<Definition name="ctx"/>
<Definition name="cst"/>
<Definition name="lprp"/>
<Definition name="inprp"/>
<Definition name="inext"/>
<Definition name="seext"/>
<Definition name="inv"/>
<Simple_Goal>
<Tag>Assertion is verified</Tag>
<Goal>
<Exp_Comparison op="=">
<Id value="empty_seq" typref="2" tag="emptyseq_1.bxml:1:4:1:1"/>
<EmptySeq typref="2" tag="emptyseq_1.bxml:1:4:1:2"/>
</Exp_Comparison>
</Goal>
</Simple_Goal>
</Proof_Obligation>
<TypeInfos>
<Type id="0">
<Unary_Exp op="POW">
<Id value="INTEGER"/>
</Unary_Exp>
</Type>
<Type id="1">
<Id value="INTEGER"/>
</Type>
<Type id="2">
<Unary_Exp op="POW">
<Binary_Exp op="*">
<Id value="INTEGER"/>
<Id value="INTEGER"/>
</Binary_Exp>
</Unary_Exp>
</Type>
<Type id="3">
<Unary_Exp op="POW">
<Unary_Exp op="POW">
<Binary_Exp op="*">
<Id value="INTEGER"/>
<Id value="INTEGER"/>
</Binary_Exp>
</Unary_Exp>
</Unary_Exp>
</Type>
</TypeInfos>
</Proof_Obligations>
Empty file added test/output/reference/emptyseq_1/stderr
View file
Open in desktop
Empty file.
Loading