Code

Examples for test generation#96

Code

Draft

yav wants to merge 153 commits intomainrems-project/cn-tutorial:mainfrom bstrems-project/cn-tutorial:bstCopy head branch name to clipboard

+2,528

Commits

Commits on Oct 15, 2024

• Fix queue pop lemma example

  

  dc-mak

  authored and

  yav

  committed
  a178c8e

  Copy full SHA for a178c8e

• timeout-broken example no-longer timing out

  

  cp526

  authored and

  yav

  committed
  4660b01

  Copy full SHA for 4660b01

• ... and move back again. Apparently different OCaml/z3 versions behave

  Show description for adb8131
  

  cp526

  authored and

  yav

  committed
  adb8131

  Copy full SHA for adb8131

• Update README.md

  Show description for 8850178
  

  dc-mak

  authored and

  yav

  committed
  8850178

  Copy full SHA for 8850178

• fix rems-project/cerberus#350

  

  cp526

  authored and

  yav

  committed
  0bbfe64

  Copy full SHA for 0bbfe64

• Add a few more small examples and error cases (#29)

  

  septract

  authored and

  yav

  committed
  1ab8504

  Copy full SHA for 1ab8504

• recategorise files with different timeout behaviour due to switch to

  Show description for f5adb3d
  

  cp526

  authored and

  yav

  committed
  f5adb3d

  Copy full SHA for f5adb3d

• Make the build script fail correctly on build errors

  

  septract

  authored and

  yav

  committed
  204c330

  Copy full SHA for 204c330

• Add negative examples in directory should-fail (#28)

  

  septract

  authored and

  yav

  committed
  3340e3b

  Copy full SHA for 3340e3b

• Add a workflow to run CN on examples

  

  septract

  authored and

  yav

  committed
  a8d390c

  Copy full SHA for a8d390c

• Properly thread through CN tool name and args

  

  septract

  authored and

  yav

  committed
  507b76b

  Copy full SHA for 507b76b

• record that one example was broken by a recent Cerberus change

  

  cp526

  authored and

  yav

  committed
  b6f95eb

  Copy full SHA for b6f95eb

• Add make check target (#14)

  Show description for 20e598f
  

  2 peopleauthored and

  yav

  committed
  20e598f

  Copy full SHA for 20e598f

• move previously-broken example back, in preparation for Kayvan's fix

  

  cp526

  authored and

  yav

  committed
  e22b93c

  Copy full SHA for e22b93c

• Add README with how to build coq lemmas

  

  scuellar

  authored and

  yav

  committed
  69a7a75

  Copy full SHA for 69a7a75

• Add examples

  

  scuellar

  authored and

  yav

  committed
  12f6e66

  Copy full SHA for 12f6e66

• Add build files

  

  scuellar

  authored and

  yav

  committed
  db0b916

  Copy full SHA for db0b916

• Add and reorder examples

  

  scuellar

  authored and

  yav

  committed
  a7d0950

  Copy full SHA for a7d0950

• Add examples and ignore automatically generated files

  

  scuellar

  authored and

  yav

  committed
  9ea5766

  Copy full SHA for 9ea5766

• Ignore more automatic coq files

  

  scuellar

  authored and

  yav

  committed
  14457db

  Copy full SHA for 14457db

• adding examples

  

  scuellar

  authored and

  yav

  committed
  f71b240

  Copy full SHA for f71b240

• Clarity

  

  scuellar

  authored and

  yav

  committed
  1cfbca2

  Copy full SHA for 1cfbca2

• Typos

  

  scuellar

  authored and

  yav

  committed
  93a6f25

  Copy full SHA for 93a6f25

• Clarify examples

  

  scuellar

  authored and

  yav

  committed
  1c88cfd

  Copy full SHA for 1c88cfd

• Add new script for checking coq extraction

  

  scuellar

  authored and

  yav

  committed
  d99d111

  Copy full SHA for d99d111

• add the script for checking coq extraction

  

  scuellar

  authored and

  yav

  committed
  4dbd8b7

  Copy full SHA for 4dbd8b7

• Explain the new organization, including Coq lemmas.

  

  scuellar

  authored and

  yav

  committed
  f50f637

  Copy full SHA for f50f637

• Generalize process_files and use it to check Coq extraction

  

  scuellar

  authored and

  yav

  committed
  f85a420

  Copy full SHA for f85a420

• Ignore the build files

  

  scuellar

  authored and

  yav

  committed
  b5b722d

  Copy full SHA for b5b722d

• Ignore coq files, except the proofs. This affects only the example-archive

  

  scuellar

  authored and

  yav

  committed
  b7e3ca0

  Copy full SHA for b7e3ca0

• Add the proofs

  

  scuellar

  authored and

  yav

  committed
  35deed9

  Copy full SHA for 35deed9

• Move examples that fail to build/incomplete proofs.

  

  scuellar

  authored and

  yav

  committed
  55e525f

  Copy full SHA for 55e525f

• Fix the popd bug and add titles to the two sections.

  

  scuellar

  authored and

  yav

  committed
  a2a431a

  Copy full SHA for a2a431a

• Move the build folder prototype to the parent directory to be used by any other examples set.

  

  scuellar

  authored and

  yav

  committed
  32b2a8c

  Copy full SHA for 32b2a8c

• Foolproof build

  

  scuellar

  authored and

  yav

  committed
  be83fa4

  Copy full SHA for be83fa4

• README details

  

  scuellar

  authored and

  yav

  committed
  6913e1e

  Copy full SHA for 6913e1e

• remove old build folder

  

  scuellar

  authored and

  yav

  committed
  f9d179f

  Copy full SHA for f9d179f

• clean up

  

  scuellar

  authored and

  yav

  committed
  7f8d632

  Copy full SHA for 7f8d632

• Fix Typos

  

  scuellar

  authored and

  yav

  committed
  be21ea3

  Copy full SHA for be21ea3

• Add clarity

  

  scuellar

  authored and

  yav

  committed
  60eb895

  Copy full SHA for 60eb895

• Tidy up typos and some script things

  

  septract

  authored and

  yav

  committed
  08667b8

  Copy full SHA for 08667b8

• Readme tweaks

  

  septract

  authored and

  yav

  committed
  47a0d5c

  Copy full SHA for 47a0d5c

• Deactivate CI for Coq to make the merge easier

  

  septract

  authored and

  yav

  committed
  ad166c5

  Copy full SHA for ad166c5

• increase timeout, for handling rems-project/cerberus#365 (comment)

  

  cp526

  authored and

  yav

  committed
  2ffc2cf

  Copy full SHA for 2ffc2cf

• recategorise that test

  

  cp526

  authored and

  yav

  committed
  bc3314a

  Copy full SHA for bc3314a

• add constructors and begin (broken) push function

  

  elaustell

  authored and

  yav

  committed
  4e3d3dd

  Copy full SHA for 4e3d3dd

• add snoc to linked list file

  

  elaustell

  authored and

  yav

  committed
  fbe03c2

  Copy full SHA for fbe03c2

• add predicates that traverse backwards

  

  elaustell

  authored and

  yav

  committed
  021b902

  Copy full SHA for 021b902

• begin implementing append (broken)

  

  elaustell

  authored and

  yav

  committed
  3f99051

  Copy full SHA for 3f99051

• create todo list

  

  elaustell

  authored and

  yav

  committed
  b0ec83e

  Copy full SHA for b0ec83e

• add constructors that go out from middle node

  

  elaustell

  authored and

  yav

  committed
  4d19bcd

  Copy full SHA for 4d19bcd

• add malloc and free

  

  elaustell

  authored and

  yav

  committed
  15a97a2

  Copy full SHA for 15a97a2

• add singleton constructor

  

  elaustell

  authored and

  yav

  committed
  f65f80d

  Copy full SHA for f65f80d

• add remove function

  

  elaustell

  authored and

  yav

  committed
  0297948

  Copy full SHA for 0297948

• include that the rest of the list is unchanged in remove function

  

  elaustell

  authored and

  yav

  committed
  73c6519

  Copy full SHA for 73c6519

• implement hacky add function

  

  elaustell

  authored and

  yav

  committed
  ae7611f

  Copy full SHA for ae7611f

• add correctness check to add_between

  

  elaustell

  authored and

  yav

  committed
  92fb603

  Copy full SHA for 92fb603

• try to implement add

  

  elaustell

  authored and

  yav

  committed
  17229f0

  Copy full SHA for 17229f0

• add comments for clarification

  

  elaustell

  authored and

  yav

  committed
  62172cf

  Copy full SHA for 62172cf

• Delete src/examples/Linked_List/WIPlinklist2.c

  

  elaustell

  authored and

  yav

  committed
  680a158

  Copy full SHA for 680a158

• add new way of reasoning about linked lists

  

  elaustell

  authored and

  yav

  committed
  7e66c47

  Copy full SHA for 7e66c47

• rework everything with opts and seqs

  

  elaustell

  authored and

  yav

  committed
  cc2a8cd

  Copy full SHA for cc2a8cd

• add simple functions with new dblList and dblListOption types

  

  elaustell

  authored and

  yav

  committed
  c84ccd2

  Copy full SHA for c84ccd2

• another attempt at add_between function

  

  elaustell

  authored and

  yav

  committed
  b22410c

  Copy full SHA for b22410c

• more work

  

  elaustell

  authored and

  yav

  committed
  4b4e445

  Copy full SHA for 4b4e445

• add remove function (working)

  

  elaustell

  authored and

  yav

  committed
  9a6b400

  Copy full SHA for 9a6b400

• work on add functions

  

  elaustell

  authored and

  yav

  committed
  4dc56cf

  Copy full SHA for 4dc56cf

• more changes

  

  elaustell

  authored and

  yav

  committed
  12953f1

  Copy full SHA for 12953f1

• Update WIPlinklist.c

  

  elaustell

  authored and

  yav

  committed
  8e2e261

  Copy full SHA for 8e2e261

• make add work

  

  elaustell

  authored and

  yav

  committed
  92e0b14

  Copy full SHA for 92e0b14

• add remove function

  

  elaustell

  authored and

  yav

  committed
  66b0572

  Copy full SHA for 66b0572

• Add correctness check for remove

  

  elaustell

  authored and

  yav

  committed
  7407333

  Copy full SHA for 7407333

• add correctness checks to add function

  

  elaustell

  authored and

  yav

  committed
  afdf2e5

  Copy full SHA for afdf2e5

• add find head and tail functions

  

  elaustell

  authored and

  yav

  committed
  1b0971e

  Copy full SHA for 1b0971e

• convert to more systematic naming conventions

  

  elaustell

  authored and

  yav

  committed
  17a8cd1

  Copy full SHA for 17a8cd1

• organize into folders and add explanations of specs

  

  elaustell

  authored and

  yav

  committed
  fddfcfc

  Copy full SHA for fddfcfc

• Change Dll datatype to only use seqs

  

  elaustell

  authored and

  yav

  committed
  1991e83

  Copy full SHA for 1991e83

• fix remove spec to be more concise

  

  elaustell

  authored and

  yav

  committed
  9a60e3a

  Copy full SHA for 9a60e3a

• rename for clarity

  

  elaustell

  authored and

  yav

  committed
  1028401

  Copy full SHA for 1028401

• change Linked_List to Dbl_Linked_list

  

  elaustell

  authored and

  yav

  committed
  e7984ff

  Copy full SHA for e7984ff

• make add spec more concise

  

  elaustell

  authored and

  yav

  committed
  16b7594

  Copy full SHA for 16b7594

• change spec identifiers to Before and After

  

  elaustell

  authored and

  yav

  committed
  3dd4f71

  Copy full SHA for 3dd4f71

• add doubly linked list to tutorial

  

  elaustell

  authored and

  yav

  committed
  2431d5c

  Copy full SHA for 2431d5c

• gitignore ./check

  

  cp526

  authored and

  yav

  committed
  5419725

  Copy full SHA for 5419725

• Update tutorial and examples for Owned disjoint

  Show description for f159166
  

  dc-mak

  authored and

  yav

  committed
  f159166

  Copy full SHA for f159166

• Temporarily delete division crash files

  Show description for 24d5748
  

  dc-mak

  authored and

  yav

  committed
  24d5748

  Copy full SHA for 24d5748

• Re-add division files

  

  dc-mak

  authored and

  yav

  committed
  e5e80ea

  Copy full SHA for e5e80ea

• add runway example to tutorial

  

  elaustell

  authored and

  yav

  committed
  e01ed1a

  Copy full SHA for e01ed1a

• Removed hard-coded repo name in CI script (#48)

  

  septract

  authored and

  yav

  committed
  7781ee6

  Copy full SHA for 7781ee6

• Create example of reading a zero-initialized array (#49)

  

  samcowger

  authored and

  yav

  committed
  9983c50

  Copy full SHA for 9983c50

• Fix #55 - Use cn verify

  

  dc-mak

  authored and

  yav

  committed
  88a8a15

  Copy full SHA for 88a8a15

• Remove redundant instantiate, add stronger post to write_5 example

  

  septract

  authored and

  yav

  committed
  3b57729

  Copy full SHA for 3b57729

• ci: install pygments gem during web deployment

  

  samcowger

  authored and

  yav

  committed
  625aaea

  Copy full SHA for 625aaea

• Move wrongly located examples

  

  septract

  authored and

  yav

  committed
  2ba6b4a

  Copy full SHA for 2ba6b4a

• Remove old annotated tutorial versions

  

  septract

  authored and

  yav

  committed
  8b24fdd

  Copy full SHA for 8b24fdd

• Modify examples to use a->b syntax

  

  septract

  authored and

  yav

  committed
  36a8c52

  Copy full SHA for 36a8c52

• Temporarily remove crashing bitwise tests

  

  dc-mak

  authored and

  yav

  committed
  8570786

  Copy full SHA for 8570786

• make asciidoc produce table of contents

  Show description for 2297bf3
  

  cp526

  authored and

  yav

  committed
  2297bf3

  Copy full SHA for 2297bf3

• Re-add bitwise complement examples (now working)

  

  dc-mak

  authored and

  yav

  committed
  8039cb4

  Copy full SHA for 8039cb4

• fix makefile to use cn verify

  

  cp526

  authored and

  yav

  committed
  386b599

  Copy full SHA for 386b599

• Quick fixes for broken build

  

  Benjamin Pierce

  authored and

  yav

  committed
  0562b8d

  Copy full SHA for 0562b8d

• Temporarily remove crashing modulo test

  

  dc-mak

  authored and

  yav

  committed
  aee33ca

  Copy full SHA for aee33ca

• recategorise now-working examples

  

  cp526

  authored and

  yav

  committed
  c9f3b4f

  Copy full SHA for c9f3b4f

• Add broken proof example from Cerberus repo here

  Show description for 7018bb7
  

  dc-mak

  authored and

  yav

  committed
  7018bb7

  Copy full SHA for 7018bb7

• Update tests for PR #459 in the Cerberus repo

  yav

  committed
  8e9c148

  Copy full SHA for 8e9c148

• put in authors, funding ack, and reference for CN paper

  

  cp526

  authored and

  yav

  committed
  7529616

  Copy full SHA for 7529616

• Tidy

  

  Benjamin Pierce

  authored and

  yav

  committed
  91198d2

  Copy full SHA for 91198d2

• recategorise some tests following Kayvan's cp526/cerberus@e0640bc

  

  cp526

  authored and

  yav

  committed
  58faff9

  Copy full SHA for 58faff9

• Temporarily remove crashing pointer dec tests

  

  dc-mak

  authored and

  yav

  committed
  596be8b

  Copy full SHA for 596be8b

• Re-add pointer dec tests

  

  dc-mak

  authored and

  yav

  committed
  18bf66c

  Copy full SHA for 18bf66c

• use cn verify in check.sh

  

  dsainati1

  authored and

  yav

  committed
  f11f32f

  Copy full SHA for f11f32f

• bump up timeout another time

  

  cp526

  authored and

  yav

  committed
  0350aa9

  Copy full SHA for 0350aa9

• update to use boolean kw, fix build script issues

  

  septract

  authored and

  yav

  committed
  19dc407

  Copy full SHA for 19dc407

• Fix more bool cases, fix Makefile

  

  septract

  authored and

  yav

  committed
  3fa9acd

  Copy full SHA for 3fa9acd

• One more instance of bool

  

  septract

  authored and

  yav

  committed
  35bedb2

  Copy full SHA for 35bedb2

• Build script tweak

  

  septract

  authored and

  yav

  committed
  d78811b

  Copy full SHA for d78811b

• Typo

  

  septract

  authored and

  yav

  committed
  4282590

  Copy full SHA for 4282590

• Fix Makefile issue

  

  septract

  authored and

  yav

  committed
  1d2bde1

  Copy full SHA for 1d2bde1

• Log SMT output from recently changed files

  

  septract

  authored and

  yav

  committed
  6445df4

  Copy full SHA for 6445df4

• Tidy up script, add comments

  

  septract

  authored and

  yav

  committed
  9860682

  Copy full SHA for 9860682

• Tweak log generator for use in CI

  

  septract

  authored and

  yav

  committed
  f0b262c

  Copy full SHA for f0b262c

• Revise script per dialog with CVC5 team

  

  septract

  authored and

  yav

  committed
  3e1592e

  Copy full SHA for 3e1592e

• Fix IntListSeg predicate

  Show description for d3b44c1
  

  dc-mak

  authored and

  yav

  committed
  d3b44c1

  Copy full SHA for d3b44c1

• Work-around Z3 bug

  Show description for b7bda5d
  

  dc-mak

  authored and

  yav

  committed
  b7bda5d

  Copy full SHA for b7bda5d

• Revert "Work-around Z3 bug"

  Show description for ff994f9
  

  dc-mak

  authored and

  yav

  committed
  ff994f9

  Copy full SHA for ff994f9

• use == instead of ptr_eq to compare u32 values (#83)

  

  dsainati1

  authored and

  yav

  committed
  c98d4ac

  Copy full SHA for c98d4ac

• bump timeout again

  

  cp526

  authored and

  yav

  committed
  24057b8

  Copy full SHA for 24057b8

• recategorise that test

  

  cp526

  authored and

  yav

  committed
  3d5cb82

  Copy full SHA for 3d5cb82

• Temporarily remove test (#87)

  Show description for f003208
  

  dc-mak

  authored and

  yav

  committed
  f003208

  Copy full SHA for f003208

• Temporarily remove test

  Show description for 3e1d0eb
  

  dc-mak

  authored and

  yav

  committed
  3e1d0eb

  Copy full SHA for 3e1d0eb

• Re-add removed broken-crash test as broken-proof

  Show description for a551d3f
  

  dc-mak

  authored and

  yav

  committed
  a551d3f

  Copy full SHA for a551d3f

• Add support for VIP

  Show description for f284ac2
  

  dc-mak

  authored and

  yav

  committed
  f284ac2

  Copy full SHA for f284ac2

• Adds style guide and naming conventions (#93)

  Show description for 7c0a52c
  

  2 peopleauthored and

  yav

  committed
  7c0a52c

  Copy full SHA for 7c0a52c

• Checkpoint: working on a binary search tree specificaion

  yav

  committed
  97366ef

  Copy full SHA for 97366ef

• Make traverse preserve the tree.

  yav

  committed
  c1858fb

  Copy full SHA for c1858fb

Commits on Oct 16, 2024

• Checkpoint: lookup with lots of duplication

  yav

  committed
  47aca9f

  Copy full SHA for 47aca9f

Commits on Oct 17, 2024

• Modify "lookup" to work in combination with "member"

  yav

  committed
  b47b8f8

  Copy full SHA for b47b8f8

Commits on Oct 23, 2024

• Some examples of using CN to generate tests

  yav

  committed
  19ede1c

  Copy full SHA for 19ede1c

Commits on Nov 4, 2024

• Merge branch 'main' into bst

  yav

  committed
  4de597e

  Copy full SHA for 4de597e

• Fix up some examples, and add sorted lists, which doesn't work at the moment

  yav

  committed
  7c46185

  Copy full SHA for 7c46185

Commits on Nov 5, 2024

• Implement a simple vector type, no CN specs yet

  yav

  committed
  fe2a505

  Copy full SHA for fe2a505

• Insertion in a sorted list

  yav

  committed
  5f8334a

  Copy full SHA for 5f8334a

• Use char as elements, and show various issues with testing.

  yav

  committed
  9bb2a8d

  Copy full SHA for 9bb2a8d

Commits on Nov 6, 2024

• Add specifications to the vector type

  yav

  committed
  b556cbd

  Copy full SHA for b556cbd

• A script to remove Etna mutants

  yav

  committed
  3456417

  Copy full SHA for 3456417

Commits on Nov 7, 2024

• Testable vector and bst

  Show description for 4f09ded
  yav

  committed
  4f09ded

  Copy full SHA for 4f09ded

• Rename to caml case

  yav

  committed
  f80fa49

  Copy full SHA for f80fa49

• Delete from BST

  yav

  committed
  c6985f5

  Copy full SHA for c6985f5

• Add a couple of mutants

  yav

  committed
  6d25b99

  Copy full SHA for 6d25b99

Commits on Nov 11, 2024

• Generate a coverage report

  yav

  committed
  2c8f00f

  Copy full SHA for 2c8f00f

• A BST formulation that separates memory layout and the invariant

  yav

  committed
  89971ed

  Copy full SHA for 89971ed

Commits on Nov 12, 2024

• Fix implementation and spec for deletion, and add specs for other operations

  yav

  committed
  045a2d7

  Copy full SHA for 045a2d7

• Fix deletion

  yav

  committed
  76168d5

  Copy full SHA for 76168d5