Code

vstd: Add no-std build mode#772

Code

Closed

zhaofengli wants to merge 10 commits intoverus-lang:mainverus-lang/verus:mainfrom mars-research:vstd-no-stdmars-research/verus:vstd-no-stdCopy head branch name to clipboard

Commits

Commits on Sep 12, 2023

• vstd/bytes: Make sure triggers are consistent

  Show description for a43d536
  zhaofengli

  committed
  a43d536

  Copy full SHA for a43d536

• vstd: Fix no-std compilation, use std and alloc features

  Show description for e4a18ff
  zhaofengli

  committed
  e4a18ff

  Copy full SHA for e4a18ff

• vstd_build: Allow disabling std and alloc

  zhaofengli

  committed
  5d6d650

  Copy full SHA for 5d6d650

• vargo: Allow disabling std and alloc in vstd

  zhaofengli

  committed
  631ff6a

  Copy full SHA for 631ff6a

Commits on Sep 18, 2023

• Revert "vstd/bytes: Make sure triggers are consistent"

  Show description for 16e45f7
  

  utaal

  authored and

  zhaofengli

  committed
  16e45f7

  Copy full SHA for 16e45f7

• fix various issues with --vstd-no-std and --vstd-no-alloc

  Show description for bb7bf7a
  

  utaal

  authored and

  zhaofengli

  committed
  bb7bf7a

  Copy full SHA for bb7bf7a

• stabilize proofs for *_to_from_le_bytes with spinoff_prover

  

  utaal

  authored and

  zhaofengli

  committed
  0ce9f9d

  Copy full SHA for 0ce9f9d

Commits on Sep 20, 2023

• vstd/vec: Allow Vec::split_off with alloc

  zhaofengli

  committed
  ea449c2

  Copy full SHA for ea449c2

• vstd/string: Support StrSlice in no-std+no-alloc

  zhaofengli

  committed
  56318b9

  Copy full SHA for 56318b9

• vstd: Pull in alloc crate once based on feature

  zhaofengli

  committed
  e33eca6

  Copy full SHA for e33eca6