Code

Advanced logical proofs#785

Code

Open

jogasser wants to merge 54 commits intoviperproject:masterviperproject/silver:masterfrom jogasser:advanced-logical-proofsjogasser/silver:advanced-logical-proofsCopy head branch name to clipboard

+2,866-38

Commits

Commits on Nov 9, 2022

• Existential Elimination v1

  dinanoe

  committed
  9c034cc

  Copy full SHA for 9c034cc

• Merge branch 'master' of https://github.com/dinanoe/silver

  dinanoe

  committed
  c229ac5

  Copy full SHA for c229ac5

• Existential Elimination added Trigger typecheck

  dinanoe

  committed
  a2c5c6d

  Copy full SHA for a2c5c6d

• Existential Elimination comments

  dinanoe

  committed
  1b56187

  Copy full SHA for 1b56187

Commits on Nov 15, 2022

• Merge branch 'viperproject:master' into master

  dinanoe

  authored
  8704df5

  Copy full SHA for 8704df5

Commits on Nov 16, 2022

• Universal Introduction v1

  dinanoe

  committed
  2eba4da

  Copy full SHA for 2eba4da

Commits on Feb 14, 2023

• Added Flow Analysis with Graph

  dinanoe

  committed
  2b2211f

  Copy full SHA for 2b2211f

Commits on Feb 25, 2023

• oldCall added, restructured Code

  dinanoe

  committed
  76ed0cd

  Copy full SHA for 76ed0cd

• merge1

  dinanoe

  committed
  37429f9

  Copy full SHA for 37429f9

Commits on Mar 21, 2023

• Complete Bachelor Thesis

  dinanoe

  committed
  2118cef

  Copy full SHA for 2118cef

Commits on Apr 16, 2023

• Merge branch 'viperproject:master' into master

  dinanoe

  authored
  ab682a9

  Copy full SHA for ab682a9

Commits on Apr 20, 2023

• Merge branch 'master' into master

  ArquintL

  authored
  437b56c

  Copy full SHA for 437b56c

Commits on Feb 28, 2024

• Merges tag 'v.24.01-release' into 'advanced-logical-proofs'

  ArquintL

  committed
  7dc7952

  Copy full SHA for 7dc7952

• fixes parser to correctly parse syntax of reasoning plugin

  ArquintL

  committed
  663797f

  Copy full SHA for 663797f

• reduces diff

  ArquintL

  committed
  abe8a9c

  Copy full SHA for abe8a9c

• adds license headers

  ArquintL

  committed
  3195a8d

  Copy full SHA for 3195a8d

• fixes a compiler error

  ArquintL

  committed
  0c0efd7

  Copy full SHA for 0c0efd7

• changes testcases that use 'heap', which is now a keyword

  ArquintL

  committed
  3da1caf

  Copy full SHA for 3da1caf

• cleans up reasoning plugin further

  ArquintL

  committed
  c217565

  Copy full SHA for c217565

• Merges branch 'master' into 'advanced-logical-proofs'

  ArquintL

  committed
  383a4df

  Copy full SHA for 383a4df

• changes yet another testcase that uses 'heap', which is now a keyword

  ArquintL

  committed
  4847f56

  Copy full SHA for 4847f56

Commits on Apr 9, 2024

• first version of graph map taint analysis

  jgaAdibilis

  committed
  7d05083

  Copy full SHA for 7d05083

Commits on Apr 16, 2024

• added assume analysis & modular method analysis

  jgaAdibilis

  committed
  4153019

  Copy full SHA for 4153019

• fix a bug in method handling & rename variables

  jgaAdibilis

  committed
  2e6d4e5

  Copy full SHA for 2e6d4e5

• ordered tests

  jgaAdibilis

  committed
  9a5b903

  Copy full SHA for 9a5b903

Commits on Apr 18, 2024

• add more tests & cleanup

  jgaAdibilis

  committed
  e558efa

  Copy full SHA for e558efa

• remove logs

  jgaAdibilis

  committed
  8e1efab

  Copy full SHA for 8e1efab

• Merge remote-tracking branch 'origin/master' into advanced-logical-proofs

  jgaAdibilis

  committed
  290bfa3

  Copy full SHA for 290bfa3

• remove todo

  jgaAdibilis

  committed
  191a812

  Copy full SHA for 191a812

• add missing position information to ImpureAssumeRewriter

  jgaAdibilis

  committed
  04de8bc

  Copy full SHA for 04de8bc

Commits on Apr 29, 2024

• fix method analysis modularity

  jgaAdibilis

  committed
  f79936a

  Copy full SHA for f79936a

Commits on May 21, 2024

• add assumesNothing spec to specify that a method contains no assume/inhale statements

  jgaAdibilis

  committed
  6d6179c

  Copy full SHA for 6d6179c

• update recursive methods & add noAssumes check

  jgaAdibilis

  committed
  b4a1086

  Copy full SHA for b4a1086

Commits on Jun 2, 2024

• Merge branch 'master' into advanced-logical-proofs

  ArquintL

  authored
  81f9b62

  Copy full SHA for 81f9b62

Commits on Jun 17, 2024

• treat non-terminating loop as assume statement & some cleanup

  jgaAdibilis

  committed
  90a763b

  Copy full SHA for 90a763b

• Merge remote-tracking branch 'origin/advanced-logical-proofs' into advanced-logical-proofs

  jgaAdibilis

  committed
  a25d1ae

  Copy full SHA for a25d1ae

• Merge remote-tracking branch 'origin/master' into advanced-logical-proofs

  jgaAdibilis

  committed
  23a3a4b

  Copy full SHA for 23a3a4b

• change position of reported error

  jgaAdibilis

  committed
  a814df4

  Copy full SHA for a814df4

Commits on Jun 24, 2024

• Update src/main/scala/viper/silver/plugin/standard/reasoning/ReasoningPlugin.scala

  Show description for cf0fea1
  

  jogasser

  and

  ArquintL

  authored
  cf0fea1

  Copy full SHA for cf0fea1

• Update src/main/scala/viper/silver/plugin/standard/reasoning/BeforeVerifyHelper.scala

  Show description for 78960ff
  

  jogasser

  and

  ArquintL

  authored
  78960ff

  Copy full SHA for 78960ff

• Update src/main/scala/viper/silver/plugin/standard/reasoning/BeforeVerifyHelper.scala

  Show description for e93fd6b
  

  jogasser

  and

  ArquintL

  authored
  e93fd6b

  Copy full SHA for e93fd6b

• Apply suggestions from code review

  Show description for 695c91b
  

  jogasser

  and

  ArquintL

  authored
  695c91b

  Copy full SHA for 695c91b

• Apply suggestions from code review

  Show description for 9bb7f88
  

  jogasser

  and

  ArquintL

  authored
  9bb7f88

  Copy full SHA for 9bb7f88

• address mr comments

  jgaAdibilis

  committed
  a0617ce

  Copy full SHA for a0617ce

• split AssumeNode into multiple AssumeNodes for better error reporting

  jgaAdibilis

  committed
  a452e1d

  Copy full SHA for a452e1d

• split veforeVerify method

  jgaAdibilis

  committed
  ab3e166

  Copy full SHA for ab3e166

• add assume to pretty print

  jgaAdibilis

  committed
  20cf3e9

  Copy full SHA for 20cf3e9

Commits on Jun 30, 2024

• improves type guarantees of modular taint analysis and fixes termination checks therein

  ArquintL

  committed
  f0476da

  Copy full SHA for f0476da

Commits on Jul 1, 2024

• fix a bug where local variables in methods were not correctly cleaned up & added test case

  jgaAdibilis

  committed
  33e0b33

  Copy full SHA for 33e0b33

• remove local variables from calculated influences before they are checked & fix some error messages

  jgaAdibilis

  committed
  1d36454

  Copy full SHA for 1d36454

Commits on Jul 2, 2024

• Merge branch 'advanced-logical-proofs' into arquintl-advanced-logical-proofs

  ArquintL

  authored
  62b2649

  Copy full SHA for 62b2649

Commits on Jul 8, 2024

• Merge pull request #1 from viperproject/arquintl-advanced-logical-proofs

  Show description for 3362648
  jogasser

  authored
  3362648

  Copy full SHA for 3362648

• remove TODO

  jgaAdibilis

  committed
  1e41b5e

  Copy full SHA for 1e41b5e

Commits on Jul 15, 2024

• add test, fix positioning & block placement

  jgaAdibilis

  committed
  8f2fa05

  Copy full SHA for 8f2fa05