Code

added harnesses for c_str: is_empty#195

Code

Closed

lanfeima wants to merge 93 commits intomodel-checking:mainmodel-checking/verify-rust-std:mainfrom rajathkotyal:c-0013-lanfeima-cstrrajathkotyal/verify-rust-std:c-0013-lanfeima-cstrCopy head branch name to clipboard

+46

Commits

Commits on Sep 11, 2024

• Add Kani proofs of unchecked_add for all integer types

  

  yew005

  committed
  1ae4c6d

  Copy full SHA for 1ae4c6d

• Format proof files & Add verification function templates

  

  yew005

  committed
  b553678

  Copy full SHA for b553678

• feat: add i8 uncheck shl verification

  MWDZ

  committed
  4db34e4

  Copy full SHA for 4db34e4

• feat: add i16 and i32 uncheck shl verification

  MWDZ

  committed
  54f5507

  Copy full SHA for 54f5507

Commits on Sep 12, 2024

• added unsafe integer i8 unchecked sub following the template

  lanfeima

  committed
  472da0e

  Copy full SHA for 472da0e

Commits on Sep 16, 2024

• Experiment with two verification approaches in mod.rs of core::num

  

  yew005

  committed
  daaaf7e

  Copy full SHA for daaaf7e

Commits on Sep 18, 2024

• Merge branch 'model-checking:main' into c-0011-core-nums-yenyunw-unsafe-ints

  Yenyun035

  authored
  7bd0e3c

  Copy full SHA for 7bd0e3c

• Add contracts to unchecked_add && Add i8::unchecked_add proof

  

  yew005

  committed
  1c9dbde

  Copy full SHA for 1c9dbde

• Format core::num mod.rs

  

  yew005

  committed
  894231f

  Copy full SHA for 894231f

• Add comment for unchecked_add proofs

  

  yew005

  committed
  2bc4faf

  Copy full SHA for 2bc4faf

Commits on Sep 19, 2024

• Add harnesses for i16,i32,i64,i128 unchecked_add

  

  yew005

  committed
  d9d4b5f

  Copy full SHA for d9d4b5f

• Add harnesses for u8,u16,u32,u64,u128 unchecked_add

  

  yew005

  committed
  07c8b4a

  Copy full SHA for 07c8b4a

• Cleanup misplaced proofs

  

  yew005

  committed
  1fd4c6a

  Copy full SHA for 1fd4c6a

Commits on Sep 20, 2024

• Clean up comment

  

  yew005

  committed
  b360311

  Copy full SHA for b360311

• Format comment

  

  yew005

  committed
  8cbca87

  Copy full SHA for 8cbca87

• Remove before contracts. Fix import in

  

  yew005

  committed
  0eef858

  Copy full SHA for 0eef858

• Fix comment

  

  yew005

  committed
  4858a53

  Copy full SHA for 4858a53

Commits on Sep 23, 2024

• Merge remote-tracking branch 'origin/c-0011-core-nums-yenyunw-unsafe-ints' into c-0011-core-nums-junfengj-unchecked-shl

  MWDZ

  committed
  8ce3381

  Copy full SHA for 8ce3381

• unchecked multiplication and shift right

  rajathkotyal

  committed
  bbd75f7

  Copy full SHA for bbd75f7

• Merge branch 'main' into c-0011-core-nums-yenyunw-unsafe-ints

  Yenyun035

  authored
  483bdf5

  Copy full SHA for 483bdf5

• Merge branch 'c-0011-core-nums-yenyunw-unsafe-ints' into c-0011-core-nums-lanfeima-unsafe-ints

  lanfeima

  committed
  71ffd37

  Copy full SHA for 71ffd37

Commits on Sep 24, 2024

• feat: add contract and test case for unchecked_shl in type int and unit

  MWDZ

  committed
  a7d3cc2

  Copy full SHA for a7d3cc2

• added preconditions and postconditions

  lanfeima

  committed
  271afad

  Copy full SHA for 271afad

• add proof functions for unchecked_sub

  lanfeima

  committed
  c7762c2

  Copy full SHA for c7762c2

• Merge branch 'model-checking:main' into c-0011-core-nums-yenyunw-unsafe-ints

  Yenyun035

  authored
  ce35002

  Copy full SHA for ce35002

• Remove ensures contracts && Undo formatting on existing code

  

  yew005

  committed
  d99844d

  Copy full SHA for d99844d

• Add {isize, usize}::unchecked_add harnesses

  

  yew005

  committed
  fbcf49e

  Copy full SHA for fbcf49e

Commits on Sep 25, 2024

• Small fix typo

  rajathkotyal

  authored
  864afa6

  Copy full SHA for 864afa6

Commits on Sep 27, 2024

• Merge branch 'model-checking:main' into c-0011-core-nums-yenyunw-unsafe-ints

  Yenyun035

  authored
  457a2b5

  Copy full SHA for 457a2b5

• Add harness generation macros for unchecked methods && Update unchecked_add harnesses

  

  yew005

  committed
  54a03ef

  Copy full SHA for 54a03ef

Commits on Sep 29, 2024

• added limits to multiplication proofs, reduced duplicacy in code by using macros to generate proof harnesses

  rajathkotyal

  committed
  ae678de

  Copy full SHA for ae678de

• Merge branch 'c-0011-core-nums-yenyunw-unsafe-ints' into c-0011-core-nums-rajathm-unsafe-ints

  rajathkotyal

  authored
  af6942e

  Copy full SHA for af6942e

Commits on Sep 30, 2024

• Remove unused import safety::ensures

  

  yew005

  committed
  8ee5682

  Copy full SHA for 8ee5682

• unchecked_mul and unchecked_shr proofs (#7)

  Show description for 02d706a
  rajathkotyal

  authored
  02d706a

  Copy full SHA for 02d706a

• Add comments. Fix spacing

  

  yew005

  committed
  dce9e83

  Copy full SHA for dce9e83

Commits on Oct 2, 2024

• Revert "Add comments. Fix spacing"

  Show description for 3880fc7
  rajathkotyal

  committed
  3880fc7

  Copy full SHA for 3880fc7

• Revert "unchecked_mul and unchecked_shr proofs (#7)"

  Show description for 781cb87
  rajathkotyal

  committed
  781cb87

  Copy full SHA for 781cb87

• Add comments. Fix spacing

  rajathkotyal

  committed
  500e8db

  Copy full SHA for 500e8db

• cleaned up code: deleted the previous attempted proofs

  lanfeima

  committed
  1c97825

  Copy full SHA for 1c97825

Commits on Oct 3, 2024

• Merge branch 'c-0011-core-nums-yenyunw-unsafe-ints' into c-0011-core-nums-lanfeima-unsafe-ints, TODO: need to handle the mod.rs conflict

  lanfeima

  committed
  4572831

  Copy full SHA for 4572831

• feat: merge the latest version

  MWDZ

  committed
  e3eb365

  Copy full SHA for e3eb365

• feat: use macro rules for unchecked_shl harness

  MWDZ

  committed
  2b3771f

  Copy full SHA for 2b3771f

• Merge branch 'c-0011-core-nums-junfengj-unchecked-shl' into c-0011-core-nums-rajathm-unsafe-ints

  MWDZ

  committed
  1a3bf40

  Copy full SHA for 1a3bf40

Commits on Oct 5, 2024

• add interval checks to unchecked_mul

  rajathkotyal

  committed
  49b0a6b

  Copy full SHA for 49b0a6b

• Merge branch 'main' into c-0011-core-nums-rajathm-unsafe-ints

  rajathkotyal

  authored
  7118fa4

  Copy full SHA for 7118fa4

• unchecked neg fix

  rajathkotyal

  committed
  bbb9656

  Copy full SHA for bbb9656

• add missing i8, i16 unchecked_mul

  rajathkotyal

  committed
  cafeea6

  Copy full SHA for cafeea6

Commits on Oct 6, 2024

• Merge branch 'c-0011-core-nums-rajathm-unsafe-ints' into c-0011-core-nums-lanfeima-unsafe-ints

  lanfeima

  committed
  51745e0

  Copy full SHA for 51745e0

• deleted the postconditions of unchecked_sub

  lanfeima

  committed
  7f4421c

  Copy full SHA for 7f4421c

• deleted the postconditions for the unchecked_sub in uint_macros

  lanfeima

  committed
  1331a77

  Copy full SHA for 1331a77

• refacted uncheck_sub harnesses

  lanfeima

  committed
  c413cac

  Copy full SHA for c413cac

Commits on Oct 11, 2024

• updated the branch with the main repository

  lanfeima

  committed
  8ce4a40

  Copy full SHA for 8ce4a40

• Add carrying_mul verification harnesses for u8, u16, u32, and u64

  lanfeima

  committed
  059dc02

  Copy full SHA for 059dc02

• updated the macro args for carrying_mult with initial carrying value

  lanfeima

  committed
  29ea0ce

  Copy full SHA for 29ea0ce

Commits on Oct 15, 2024

• resolved the compile error for carrying_mul

  lanfeima

  committed
  6f7deae

  Copy full SHA for 6f7deae

• deleted the kani submodule for merge

  lanfeima

  committed
  ad031a1

  Copy full SHA for ad031a1

• formatted the style

  lanfeima

  committed
  ddabe95

  Copy full SHA for ddabe95

Commits on Oct 18, 2024

• Added documentation for generate_carrying_mul_intervals macro

  lanfeima

  committed
  27522b4

  Copy full SHA for 27522b4

Commits on Oct 19, 2024

• added full range interval for u8 and u16

  lanfeima

  committed
  604d746

  Copy full SHA for 604d746

Commits on Oct 20, 2024

• reduced the interval for carrying_mul u32,u64

  lanfeima

  committed
  71399d8

  Copy full SHA for 71399d8

Commits on Oct 22, 2024

• f32 test harness & contracts

  Yenyun035

  committed
  95d11f3

  Copy full SHA for 95d11f3

Commits on Oct 23, 2024

• Merge branch 'model-checking:main' into c-0011-core-nums-yenyunw-f32-to-int-unchecked

  Yenyun035

  authored
  88f7363

  Copy full SHA for 88f7363

Commits on Oct 24, 2024

• Fix contracts && Initial draft of macro and harnesses

  Yenyun035

  committed
  227d9ac

  Copy full SHA for 227d9ac

• Merge branch 'model-checking:main' into c-0011-core-nums-yenyunw-f32-to-int-unchecked

  Yenyun035

  authored
  b875696

  Copy full SHA for b875696

Commits on Oct 25, 2024

• Merge branch 'main' into c-0011-core-nums-lanfeim-carrying-mul

  rajathkotyal

  authored
  1253264

  Copy full SHA for 1253264

Commits on Oct 26, 2024

• Merge main

  Yenyun035

  committed
  70fe5d9

  Copy full SHA for 70fe5d9

Commits on Oct 28, 2024

• Merge branch 'main' of github.com:rajathkotyal/verify-rust-std into c-0011-core-nums-yenyunw-f32-to-int-unchecked

  Yenyun035

  committed
  5742a89

  Copy full SHA for 5742a89

Commits on Oct 30, 2024

• f128_float_to_int proofs

  rajathkotyal

  committed
  082ea5a

  Copy full SHA for 082ea5a

• Fix comment

  Yenyun035

  committed
  bb00a72

  Copy full SHA for bb00a72

• Merge branch 'model-checking:main' into c-0011-core-nums-yenyunw-f32-to-int-unchecked

  Yenyun035

  authored
  88c3411

  Copy full SHA for 88c3411

• Merge branch 'main' into c-0011-core-nums-yenyunw-f32-to-int-unchecked

  Yenyun035

  authored
  a661c16

  Copy full SHA for a661c16

Commits on Oct 31, 2024

• Merge branch 'model-checking:main' into c-0011-core-nums-yenyunw-f32-to-int-unchecked

  Yenyun035

  authored
  c85ce2a

  Copy full SHA for c85ce2a

Commits on Nov 2, 2024

• Merge remote-tracking branch 'origin/c-0011-core-nums-yenyunw-f32-to-int-unchecked' into c-0011-core-nums-lanfeim-f16-to-int-unchecked

  lanfeima

  committed
  02a8b0c

  Copy full SHA for 02a8b0c

• added the contracts and harnesses for f16-int_unchecked

  lanfeima

  committed
  3e9613b

  Copy full SHA for 3e9613b

Commits on Nov 22, 2024

• Test CStr safety invariant

  Yenyun035

  committed
  bf613a0

  Copy full SHA for bf613a0

• Merge branch 'model-checking:main' into c-0013-yenyunw-cstr

  Yenyun035

  authored
  cf6aab1

  Copy full SHA for cf6aab1

• Merge branch 'model-checking:main' into c-0013-yenyunw-cstr

  Yenyun035

  authored
  63d53fb

  Copy full SHA for 63d53fb

• Add CStr safety invariant && from_bytes_until_null harnesses

  Yenyun035

  committed
  90ae7a5

  Copy full SHA for 90ae7a5

• Merge branch 'model-checking:main' into c-0013-yenyunw-cstr

  Yenyun035

  authored
  e111145

  Copy full SHA for e111145

• Add comments

  Yenyun035

  committed
  55dfaaf

  Copy full SHA for 55dfaaf

Commits on Nov 23, 2024

• Merge remote-tracking branch 'origin/c-0013-yenyunw-cstr' into c-0013-lanfeima-cstr

  lanfeima

  committed
  3b01c6b

  Copy full SHA for 3b01c6b

• merge recent cstr

  lanfeima

  committed
  b49f4ee

  Copy full SHA for b49f4ee

• added harnesses for is_empty

  lanfeima

  committed
  f03b418

  Copy full SHA for f03b418

Commits on Nov 27, 2024

• Add to_bytes and to_bytes_with_nul harnesses

  Yenyun035

  committed
  64ddbff

  Copy full SHA for 64ddbff

• Merge remote-tracking branch 'origin/c-0013-yenyunw-cstr-to-bytes' into c-0013-lanfeima-cstr

  lanfeima

  committed
  90865ea

  Copy full SHA for 90865ea

• combined the is_empty with the latest repo

  lanfeima

  committed
  1fc9540

  Copy full SHA for 1fc9540

Commits on Nov 28, 2024

• finished testing for is_empty

  lanfeima

  committed
  7e75de1

  Copy full SHA for 7e75de1

• used kani_anywhere to generate the values

  lanfeima

  committed
  ae7af7c

  Copy full SHA for ae7af7c

• edited the documentation

  lanfeima

  committed
  43e588c

  Copy full SHA for 43e588c

• remove the irrelevant kani folder and cargo file

  lanfeima

  committed
  fdefcc0

  Copy full SHA for fdefcc0

• reverted Cargo.lock to the stable one

  lanfeima

  authored
  1f5e28a

  Copy full SHA for 1f5e28a

• Reset stdarch submodule to commit ff9a444

  lanfeima

  committed
  8cc0b12

  Copy full SHA for 8cc0b12

Commits on Nov 29, 2024

• revised is_empty harness without using arbitrary_cstr

  lanfeima

  committed
  41ddead

  Copy full SHA for 41ddead