Skip to content

Commit

Permalink
fix spec file
Browse files Browse the repository at this point in the history
  • Loading branch information
ailrst committed Oct 18, 2023
1 parent 20f4b81 commit a385218
Showing 1 changed file with 5 additions and 5 deletions.
10 changes: 5 additions & 5 deletions examples/simplified_http_parse_basic/example.spec
Original file line number Diff line number Diff line change
Expand Up @@ -8,11 +8,11 @@ DIRECT functions: gamma_load64, gamma_load8, memory_load8_le, bvult64, bvule64,


Subroutine: #free
Requires DIRECT: "gamma_load8(Gamma_mem, bvadd64(R0, 0bv64)) == true";
Requires DIRECT: "gamma_load8(Gamma_mem, bvadd64(R0, 1bv64)) == true";
Requires DIRECT: "gamma_load8(Gamma_mem, bvadd64(R0, 2bv64)) == true";
Requires DIRECT: "gamma_load8(Gamma_mem, bvadd64(R0, 3bv64)) == true";
Ensures DIRECT: "Gamma_R0 == true"
Requires DIRECT: "gamma_load8(Gamma_mem, bvadd64(R0, 0bv64)) == true"
Requires DIRECT: "gamma_load8(Gamma_mem, bvadd64(R0, 1bv64)) == true"
Requires DIRECT: "gamma_load8(Gamma_mem, bvadd64(R0, 2bv64)) == true"
Requires DIRECT: "gamma_load8(Gamma_mem, bvadd64(R0, 3bv64)) == true"
Ensures DIRECT: "Gamma_R0 == true"


Subroutine: main
Expand Down

0 comments on commit a385218

Please sign in to comment.