Unverified Commit 7e5ea885 authored by Nadim Kobeissi's avatar Nadim Kobeissi 💎

Add basic bindings for Coq

parent fc6f7dd7
Pipeline #50 failed with stages
in 12 seconds
......@@ -3,8 +3,6 @@ run:
- parser.go
- main_test.go
- help.go
- coq.go
- proverif.go
linters:
enable:
......
......@@ -45,6 +45,8 @@ func mainGanbatte(args []string) {
verifpal.Verify(args[2])
case "proverif":
verifpal.ProVerif(args[2])
case "coq":
verifpal.Coq(args[2])
case "pretty":
verifpal.PrettyPrint(args[2])
case "implement":
......
......@@ -4,6 +4,7 @@
package verifpal
func coq(m Model) {
// Coq translates a Verifpal model into a representation that fits into the Coq model of the Verifpal verification methodology.
func Coq(modelFile string) {
errorCritical("this feature does not exist yet")
}
......@@ -14,11 +14,11 @@ import (
// Help displays Verifpal command-line usage instructions.
func Help(a string) {
fmt.Fprintf(os.Stdout, "%s\n%s\n%s\n%s\n%s\n",
"verify [file]: Load and analyze Verifpal model from file.",
"proverif [file]: Translate a Verifpal model into a ProVerif model.",
"verify [file]: Analyze Verifpal model.",
"proverif [file]: Translate Verifpal model into ProVerif model.",
"pretty [file]: Pretty-print Verifpal model.",
"implement [file]: Implement Verifpal model in Go.",
"help: Show this help text.",
"implement [file]: Translate Verifpal model into Go implementation.",
"help : Show this help text.",
)
x := make([]byte, 07)
y := make([]byte, 38)
......
......@@ -10,6 +10,7 @@ import (
"strings"
)
// ProVerif translates a Verifpal model into a ProVerif model.
func ProVerif(modelFile string) {
m := parserParseModel(modelFile, false)
sanity(m)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment