Commit 5fa5cde

committed

Mar 10, 2025

Moving CN to its own repository

This commit removes all non-cn files and is based on commit 60fbd00 from the cerberus repo.

1 parent af50626 commit 5fa5cdeCopy full SHA for 5fa5cde

7,685 files changed

+220

-859478

lines changed

.gitattributes
.github/workflows
- ci-cheri.yml
- ci-cn-bench.yml
- ci-cn-coq.yml
- ci-cn-spec-testing.yml
- ci-cn.yml
- ci-pr-bench.yml.disabled
- ci.yml
.gitignore
.ocamlformat
CN-COQ.md
CONTRIBUTING.md
Dockerfile.cheri
Dockerfile.redhat
Dockerfile.ubuntu
FULMINATE_README.md
LICENSE
Makefile
ONBOARDING.md
PROFILING.md
README-cheri.md
README.md
SWITCHES
TESTING.md
THIRD_PARTY_FILES.md
_CoqProject
backend
- absint
- ail_playground
  - dune
  - main.ml
- bmc
- cn
  - README.md
  - coq
    - dune
  - dune
- common
- driver
- ocaml
  - README.md
  - driver
  - runtime
- playground
  - dune
  - main.ml
  - src
    - simpl.ml
  - tests
    - a.c
    - a.core
- rustic
  - dune
  - examples
    - attr_on_empty_statement.c
  - main.ml
  - src
- web
bin
- dune
- main.ml
cerberus-absint.opam
cerberus-bmc.opam
cerberus-cheri.opam
cerberus-lib.opam
cerberus-ocaml.opam
cerberus-web.opam
cerberus.opam
cn-coq.opam
cn.opam
coq
- .gitignore
- Cerberus
- CheriMemory
- Cn
- Common
- Morello
- Proofs
- Reasoning
- coqcaptest.ml
- dune
- extracted
- strfcap.ml
dune
dune-project
dune-workspace.profiling
frontend
- concurrency
- model
- ott
- proof
  - coq
  - hol
generated_tex
- lem.sty
lib
- alloc.ml
- alloc.mli
- argumentTypes.ml
- baseTypes.ml
- bugExplanation
  - bugExplanation.ml
  - bugExplanation.mli
  - replicators.ml
  - replicators.mli
  - shapeAnalyzers.ml
  - shapeAnalyzers.mli
- builtins.ml
- cLogicalFuns.ml
- cStatements.ml
- check.ml
- checkPredicates.ml
- cn_internal_to_ail.ml
- cn_internal_to_ail.mli
- cnprog.ml
- compile.ml
- consistent.ml
- consistent.mli
- context.ml
- context.mli
- coreTypeChecks.ml
- core_to_mucore.ml
- core_to_mucore.mli
- definition.ml
- definition.mli
- diagnostics.ml
- dune
- effectful.ml
- eqTable.ml
- error_common.ml
- executable_spec.ml
- executable_spec_extract.ml
- executable_spec_extract.mli
- executable_spec_internal.ml
- executable_spec_records.ml
- executable_spec_utils.ml
- explain.ml
- explain.mli
- false.ml
- false.mli
- global.ml
- id.ml
- id.mli
- indexTerms.ml
- interval.ml
- interval.mli
- lemmata.ml
- list.ml
- locations.ml
- locations.mli
- logicalArgumentTypes.ml
- logicalConstraints.ml
- logicalConstraints.mli
- logicalReturnTypes.ml
- memory.ml
- mucore.ml
- mucore.mli
- option.ml
- or_TypeError.ml
- ownership_exec.ml
- pack.ml
- parse.ml
- pp.ml
- pp.mli
- pp_mucore.ml
- pp_mucore_ast.ml
- pp_mucore_coq.ml
- prooflog.ml
- prooflog.mli
- report.ml
- report.mli
- request.ml
- request.mli
- resource.ml
- resource.mli
- resourceInference.ml
- resourceInference.mli
- resultWithData.ml
- returnTypes.ml
- sctypes.ml
- setup.ml
- setup.mli
- simple_smt.ml
- simplify.ml
- solver.ml
- solver.mli
- source_injection.ml
- source_injection.mli
- style.ml
- style.mli
- subst.ml
- sym.ml
- terms.ml
- testGeneration
  - buildScript.ml
  - buildScript.mli
  - genAnalysis.ml
  - genBaseTypes.ml
  - genBuiltins.ml
  - genCodeGen.ml
  - genCodeGen.mli
  - genCompile.ml
  - genCompile.mli
  - genDefinitions.ml
  - genDistribute.ml
  - genDistribute.mli
  - genInline.ml
  - genNormalize.ml
  - genNormalize.mli
  - genOptimize.ml
  - genRuntime.ml
  - genRuntime.mli
  - genStatements.ml
  - genTerms.ml
  - genUtils.ml
  - seqTestGenConfig.ml
  - seqTestGenConfig.mli
  - seqTests.ml
  - seqTests.mli
  - specTests.ml
  - specTests.mli
  - test.ml
  - testGenConfig.ml
  - testGenConfig.mli
  - testGeneration.ml
  - testGeneration.mli
- tools.ml
- typeErrors.ml
- typeErrors.mli
- typing.ml
- typing.mli
- wellTyped.ml
- wellTyped.mli
- wellTyped_intf.ml
- where.ml
- where.mli
manual
- Makefile
- grammar.md
- logic.md
- manual.html
- manual.md
memory
- cheri-coq
  - dune
  - impl_mem.ml
- concrete
- dune
- symbolic
- vip
ocaml_frontend
- ail_analysis.ml
- ail_analysis.mli
- cn_ocaml.ml
- core_remove_unused_functions.ml
- decode.ml
- dune
- impl_mem.mli
- memory_model.ml
- memory_utils.ml
- milicore.ml
- milicore_label_inline.ml
- ocaml_gcc_builtins.ml
- ocaml_implementation.ml
- ocaml_implementation.mli
- pprinters
  - ast_core.ml
  - pp_ail.ml
  - pp_ail.mli
  - pp_ail_ast.ml
  - pp_ail_raw.ml
  - pp_ast.ml
  - pp_cabs.ml
  - pp_cabs.mli
  - pp_cabs0.ml_UNUSED
  - pp_cmm.ml
  - pp_cmm.mli
  - pp_constraints.ml
  - pp_core.ml
  - pp_core.mli
  - pp_core_ast.ml
  - pp_core_ctype.ml
  - pp_defacto_memory.ml
  - pp_defacto_memory.mli
  - pp_errors.ml
  - pp_mem.ml
  - pp_mem.mli
  - pp_naive_memory.ml
  - pp_naive_memory.mli
  - pp_run.ml
  - pp_sb.ml
  - pp_std.ml
  - pp_symbol.ml
  - pp_symbol.mli
  - pp_symbolic.ml
  - pp_symbolic.mli
  - pp_trace.ml
  - pp_utils.ml
  - string_ail.ml
  - string_cabs.ml
  - string_core.ml
  - string_core_ctype.ml
  - string_core_run.ml
  - string_defacto_memory.ml
  - string_mem.ml
  - string_nat_big_num.ml
  - string_nat_big_num.mli
  - string_symbol.ml
- rewriters
  - core_peval.ml
  - core_rewriter.ml
  - identity_monad.ml
  - remove_unspecs.ml
- smt2.ml
- switches.ml
- switches.mli
- tags.ml
- tags.mli
parsers
- c
- core
public
- Makefile
- README.md
- deploy.sh
- dev.config.js
- dist
- package.json
- preprocessor.js
- prod.config.js
- src
- tests
  - ui-test.js
- tsconfig.json
runtime
- bmc
- dune
- libc
  - dune
  - generators
    - gen_inttypes.c
  - include
    - assert.h
    - builtins.h
    - cerberus
      - any.h
      - vip.h
    - cheri
      - cheric.h
    - cheriintrin.h
    - complex.h
    - ctype.h
    - errno.h
    - fenv.h
    - float.h
    - inttypes.h
    - iso646.h
    - limits.h
    - locale.h
    - math.h
    - posix
      - aio.h
      - arpa
        inet.h
      - assert.h
      - complex.h
      - cpio.h
      - ctype.h
      - dirent.h
      - dlfcn.h
      - errno.h
      - fcntl.h
      - fenv.h
      - float.h
      - fmtmsg.h
      - fnmatch.h
      - ftw.h
      - glob.h
      - grp.h
      - iconv.h
      - inttypes.h
      - iso646.h
      - langinfo.h
      - libgen.h
      - limits.h
      - locale.h
      - math.h
      - monetary.h
      - mqueue.h
      - ndbm.h
      - net
        if.h
      - netdb.h
      - netinet
        in.h
        tcp.h
      - nl_types.h
      - poll.h
      - pthread.h
      - pwd.h
      - regex.h
      - sched.h
      - search.h
      - semaphore.h
      - setjmp.h
      - signal.h
      - spawn.h
      - stdarg.h
      - stdbool.h
      - stddef.h
      - stdint.h
      - stdio.h
      - stdlib.h
      - string.h
      - strings.h
      - stropts.h
      - sys
        cdefs.h
        ioctl.h
        ipc.h
        mman.h
        msg.h
        resource.h
        select.h
        sem.h
        shm.h
        socket.h
        stat.h
        statvfs.h
        time.h
        times.h
        types.h
        uio.h
        un.h
        utsname.h
        wait.h
      - syslog.h
      - tar.h
      - termios.h
      - tgmath.h
      - time.h
      - trace.h
      - ulimit.h
      - unistd.h
      - utime.h
      - utmpx.h
      - wchar.h
      - wctype.h
      - wordexp.h
    - setjmp.h
    - signal.h
    - stdalign.h
    - stdarg.h
    - stdatomic.h
    - stdbool.h
    - stddef.h
    - stdint.h
    - stdio.h
    - stdlib.h
    - stdnoreturn.h
    - string.h
    - tgmath.h
    - threads.h
    - time.h
    - uchar.h
    - wchar.h
    - wctype.h
  - src
- libcore
rustic.opam
sibylfs
- LICENSE
- README.md
- dune
- original
- patch
- patch_all_ml.sed
- src
tests
- README
- README_KCC_SUITE
- bmc
- cheri-ci
- ci
- cn-seq-test-gen
  - .DS_Store
- common.sh
- core
  - ahem.core
- csmith
  - runtime
  - small_arrays

7,685 files changed

+220

-859478

lines changed

`‎.gitattributes`

-1

This file was deleted.

`‎.github/workflows/ci-cheri.yml`

-80

This file was deleted.

Comments

(0)

Please sign in to comment.