Skip to content
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.

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

Advanced logical proofs #785

Open
wants to merge 54 commits into
base: master
Choose a base branch
from
Open
Changes from 1 commit
Commits
Show all changes
54 commits
Select commit Hold shift + click to select a range
9c034cc
Existential Elimination v1
dinanoe Nov 9, 2022
c229ac5
Merge branch 'master' of https://github.com/dinanoe/silver
dinanoe Nov 9, 2022
a2c5c6d
Existential Elimination added Trigger typecheck
dinanoe Nov 9, 2022
1b56187
Existential Elimination comments
dinanoe Nov 9, 2022
8704df5
Merge branch 'viperproject:master' into master
dinanoe Nov 15, 2022
2eba4da
Universal Introduction v1
dinanoe Nov 16, 2022
2b2211f
Added Flow Analysis with Graph
dinanoe Feb 14, 2023
76ed0cd
oldCall added, restructured Code
dinanoe Feb 25, 2023
37429f9
merge1
dinanoe Feb 25, 2023
2118cef
Complete Bachelor Thesis
dinanoe Mar 21, 2023
ab682a9
Merge branch 'viperproject:master' into master
dinanoe Apr 16, 2023
437b56c
Merge branch 'master' into master
ArquintL Apr 20, 2023
7dc7952
Merges tag 'v.24.01-release' into 'advanced-logical-proofs'
ArquintL Feb 28, 2024
663797f
fixes parser to correctly parse syntax of reasoning plugin
ArquintL Feb 27, 2024
abe8a9c
reduces diff
ArquintL Feb 27, 2024
3195a8d
adds license headers
ArquintL Feb 27, 2024
0c0efd7
fixes a compiler error
ArquintL Feb 27, 2024
3da1caf
changes testcases that use 'heap', which is now a keyword
ArquintL Feb 27, 2024
c217565
cleans up reasoning plugin further
ArquintL Feb 28, 2024
383a4df
Merges branch 'master' into 'advanced-logical-proofs'
ArquintL Feb 28, 2024
4847f56
changes yet another testcase that uses 'heap', which is now a keyword
ArquintL Feb 28, 2024
7d05083
first version of graph map taint analysis
jgaAdibilis Apr 9, 2024
4153019
added assume analysis & modular method analysis
jgaAdibilis Apr 16, 2024
2e6d4e5
fix a bug in method handling & rename variables
jgaAdibilis Apr 16, 2024
9a5b903
ordered tests
jgaAdibilis Apr 16, 2024
e558efa
add more tests & cleanup
jgaAdibilis Apr 18, 2024
8e1efab
remove logs
jgaAdibilis Apr 18, 2024
290bfa3
Merge remote-tracking branch 'origin/master' into advanced-logical-pr…
jgaAdibilis Apr 18, 2024
191a812
remove todo
jgaAdibilis Apr 18, 2024
04de8bc
add missing position information to ImpureAssumeRewriter
jgaAdibilis Apr 18, 2024
f79936a
fix method analysis modularity
jgaAdibilis Apr 29, 2024
6d6179c
add assumesNothing spec to specify that a method contains no assume/i…
jgaAdibilis May 21, 2024
b4a1086
update recursive methods & add noAssumes check
jgaAdibilis May 21, 2024
81f9b62
Merge branch 'master' into advanced-logical-proofs
ArquintL Jun 2, 2024
90a763b
treat non-terminating loop as assume statement & some cleanup
jgaAdibilis Jun 17, 2024
a25d1ae
Merge remote-tracking branch 'origin/advanced-logical-proofs' into ad…
jgaAdibilis Jun 17, 2024
23a3a4b
Merge remote-tracking branch 'origin/master' into advanced-logical-pr…
jgaAdibilis Jun 17, 2024
a814df4
change position of reported error
jgaAdibilis Jun 17, 2024
cf0fea1
Update src/main/scala/viper/silver/plugin/standard/reasoning/Reasonin…
jogasser Jun 24, 2024
78960ff
Update src/main/scala/viper/silver/plugin/standard/reasoning/BeforeVe…
jogasser Jun 24, 2024
e93fd6b
Update src/main/scala/viper/silver/plugin/standard/reasoning/BeforeVe…
jogasser Jun 24, 2024
695c91b
Apply suggestions from code review
jogasser Jun 24, 2024
9bb7f88
Apply suggestions from code review
jogasser Jun 24, 2024
a0617ce
address mr comments
jgaAdibilis Jun 24, 2024
a452e1d
split AssumeNode into multiple AssumeNodes for better error reporting
jgaAdibilis Jun 24, 2024
ab3e166
split veforeVerify method
jgaAdibilis Jun 24, 2024
20cf3e9
add assume to pretty print
jgaAdibilis Jun 24, 2024
f0476da
improves type guarantees of modular taint analysis and fixes terminat…
ArquintL Jun 30, 2024
33e0b33
fix a bug where local variables in methods were not correctly cleaned…
jgaAdibilis Jul 1, 2024
1d36454
remove local variables from calculated influences before they are che…
jgaAdibilis Jul 1, 2024
62b2649
Merge branch 'advanced-logical-proofs' into arquintl-advanced-logical…
ArquintL Jul 2, 2024
3362648
Merge pull request #1 from viperproject/arquintl-advanced-logical-proofs
jogasser Jul 8, 2024
1e41b5e
remove TODO
jgaAdibilis Jul 8, 2024
8f2fa05
add test, fix positioning & block placement
jgaAdibilis Jul 15, 2024
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
Prev Previous commit
Next Next commit
remove TODO
jgaAdibilis committed Jul 8, 2024
commit 1e41b5ed31b138a284e5b6b8ee1fcbb4ee6fe15d
Original file line number Diff line number Diff line change
@@ -503,7 +503,6 @@ case class VarAnalysisGraphMap(prog: Program,
case UnExp(exp) => getSinksFromExpr(exp)
case f: FuncApp =>
val isHeapDependent = Expressions.couldBeHeapDependent(f.func(prog), prog)
// TODO: do we need to filter out Refs?
f.args.flatMap(e => getSinksFromExpr(e)).toSet ++ (if (isHeapDependent) Set(HeapSink) else Set.empty)
case DomainFuncApp(_, exps, _) => exps.flatMap(e => getSinksFromExpr(e)).toSet
case _: ForPerm | _: CurrentPerm => Set(HeapSink)