Mentions légales du service
Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
why3
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Deploy
Releases
Container registry
Monitor
Service Desk
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
Why3
why3
Commits
12633d91
Commit
12633d91
authored
7 years ago
by
Raphaël Rieu-Helft
Browse files
Options
Downloads
Patches
Plain Diff
Update C driver
parent
ae988660
No related branches found
No related tags found
No related merge requests found
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
drivers/c.drv
+66
-24
66 additions, 24 deletions
drivers/c.drv
with
66 additions
and
24 deletions
drivers/c.drv
+
66
−
24
View file @
12633d91
...
@@ -39,6 +39,32 @@ module mach.int.Int32
...
@@ -39,6 +39,32 @@ module mach.int.Int32
syntax val (>) "%1 > %2"
syntax val (>) "%1 > %2"
end
end
module mach.int.UInt32Gen
syntax type uint32 "uint32_t"
syntax converter max_uint32 "0xffffffff"
syntax converter length "32"
end
module mach.int.UInt32
syntax converter of_int "%1U"
syntax val (+) "%1 + %2"
syntax val (-) "%1 - %2"
syntax val (*) "%1 * %2"
syntax val (/) "%1 / %2"
syntax val (%) "%1 % %2"
syntax val (=) "%1 == %2"
syntax val (<=) "%1 <= %2"
syntax val (<) "%1 < %2"
syntax val (>=) "%1 >= %2"
syntax val (>) "%1 > %2"
end
module mach.int.UInt32GMP
module mach.int.UInt32GMP
prelude
prelude
...
@@ -119,17 +145,6 @@ struct __lsld32_result lsld32(uint32_t x, uint32_t cnt)
...
@@ -119,17 +145,6 @@ struct __lsld32_result lsld32(uint32_t x, uint32_t cnt)
syntax converter of_int "%1U"
syntax converter of_int "%1U"
syntax type uint32 "uint32_t"
syntax converter max_uint32 "0xffffffff"
syntax converter length "32"
syntax val add_with_carry "add32_with_carry"
syntax val sub_with_borrow "sub32_with_borrow"
syntax val mul_double "mul32_double"
syntax val add3 "add32_3"
syntax val lsld "lsld32"
syntax val (+) "%1 + %2"
syntax val (+) "%1 + %2"
syntax val (-) "%1 - %2"
syntax val (-) "%1 - %2"
syntax val (*) "%1 * %2"
syntax val (*) "%1 * %2"
...
@@ -141,6 +156,12 @@ struct __lsld32_result lsld32(uint32_t x, uint32_t cnt)
...
@@ -141,6 +156,12 @@ struct __lsld32_result lsld32(uint32_t x, uint32_t cnt)
syntax val (>=) "%1 >= %2"
syntax val (>=) "%1 >= %2"
syntax val (>) "%1 > %2"
syntax val (>) "%1 > %2"
syntax val add_with_carry "add32_with_carry"
syntax val sub_with_borrow "sub32_with_borrow"
syntax val mul_double "mul32_double"
syntax val add3 "add32_3"
syntax val lsld "lsld32"
syntax val add_mod "%1 + %2"
syntax val add_mod "%1 + %2"
syntax val sub_mod "%1 - %2"
syntax val sub_mod "%1 - %2"
syntax val mul_mod "%1 * %2"
syntax val mul_mod "%1 * %2"
...
@@ -158,6 +179,33 @@ struct __lsld32_result lsld32(uint32_t x, uint32_t cnt)
...
@@ -158,6 +179,33 @@ struct __lsld32_result lsld32(uint32_t x, uint32_t cnt)
syntax val of_int32 "(uint32_t)%1"
syntax val of_int32 "(uint32_t)%1"
end
module mach.int.UInt64Gen
syntax type uint64 "uint64_t"
syntax converter max_uint64 "0xffffffffffffffff"
syntax converter length "64"
end
module mach.int.UInt64
syntax converter of_int "%1ULL"
syntax val (+) "%1 + %2"
syntax val (-) "%1 - %2"
syntax val (*) "%1 * %2"
syntax val (/) "%1 / %2"
syntax val (%) "%1 % %2"
syntax val (=) "%1 == %2"
syntax val (<=) "%1 <= %2"
syntax val (<) "%1 < %2"
syntax val (>=) "%1 >= %2"
syntax val (>) "%1 > %2"
end
end
module mach.int.UInt64GMP
module mach.int.UInt64GMP
...
@@ -257,18 +305,6 @@ struct __lsld64_result lsld64(uint64_t x, uint64_t cnt)
...
@@ -257,18 +305,6 @@ struct __lsld64_result lsld64(uint64_t x, uint64_t cnt)
syntax converter of_int "%1ULL"
syntax converter of_int "%1ULL"
syntax type uint64 "uint64_t"
syntax converter max_uint64 "0xffffffffffffffff"
syntax converter length "64"
syntax val add_with_carry "add64_with_carry"
syntax val sub_with_borrow "sub64_with_borrow"
syntax val mul_double "mul64_double"
syntax val div2by1 "div64_2by1"
syntax val add3 "add64_3"
syntax val lsld "lsld64"
syntax val (+) "%1 + %2"
syntax val (+) "%1 + %2"
syntax val (-) "%1 - %2"
syntax val (-) "%1 - %2"
syntax val (*) "%1 * %2"
syntax val (*) "%1 * %2"
...
@@ -280,6 +316,13 @@ struct __lsld64_result lsld64(uint64_t x, uint64_t cnt)
...
@@ -280,6 +316,13 @@ struct __lsld64_result lsld64(uint64_t x, uint64_t cnt)
syntax val (>=) "%1 >= %2"
syntax val (>=) "%1 >= %2"
syntax val (>) "%1 > %2"
syntax val (>) "%1 > %2"
syntax val add_with_carry "add64_with_carry"
syntax val sub_with_borrow "sub64_with_borrow"
syntax val mul_double "mul64_double"
syntax val div2by1 "div64_2by1"
syntax val add3 "add64_3"
syntax val lsld "lsld64"
syntax val add_mod "%1 + %2"
syntax val add_mod "%1 + %2"
syntax val sub_mod "%1 - %2"
syntax val sub_mod "%1 - %2"
syntax val mul_mod "%1 * %2"
syntax val mul_mod "%1 * %2"
...
@@ -293,7 +336,6 @@ struct __lsld64_result lsld64(uint64_t x, uint64_t cnt)
...
@@ -293,7 +336,6 @@ struct __lsld64_result lsld64(uint64_t x, uint64_t cnt)
syntax val of_int32 "(uint64_t)%1"
syntax val of_int32 "(uint64_t)%1"
end
end
...
...
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment