List view

C-FFI: Set of test-cases for FFI linking

[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.

Status: Open.

#2150 In model-checking/kani;

· danielsn opened on Jan 24, 2023

C-FFI: Support for void vs unit return type in CBMC linker

[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.

Status: Open.

#2151 In model-checking/kani;

· danielsn opened on Jan 24, 2023

Support for variadic extern function calls

[C] BugThis is a bug. Something isn't working.This is a bug. Something isn't working.

Status: Open.

Bug

#72 In model-checking/kani;

· adpaco opened on Apr 16, 2021

C-FFI: support build of C files using build.rs

[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.

Status: Open.

#2153 In model-checking/kani;

· danielsn opened on Jan 24, 2023

Rethink naming for external C libraries

[C] BugThis is a bug. Something isn't working.This is a bug. Something isn't working.

Status: Open.

Bug

#450 In model-checking/kani;

· avanhatt opened on Aug 25, 2021

Add proper support to C-FFI calls

[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.

T-UserTag user issues / requestsTag user issues / requests

Status: Open.

#2423 In model-checking/kani;

· celinval opened on May 2, 2023

Option<&foo> does not decay to *foo in extern C mode

[C] BugThis is a bug. Something isn't working.This is a bug. Something isn't working.

[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.

Status: Open.

Bug

#3 In model-checking/kani;

· danielsn opened on Mar 29, 2021

Kani should verify the existance of clashing C functions

[C] BugThis is a bug. Something isn't working.This is a bug. Something isn't working.

Status: Open.

Bug

#2426 In model-checking/kani;

· celinval opened on May 3, 2023

_tlv_atexit definition is missing

[C] BugThis is a bug. Something isn't working.This is a bug. Something isn't working.

Status: Open.

Bug

#2430 In model-checking/kani;

· adpaco opened on May 4, 2023

Integrate mmap model from CBMC

[E] Unsupported ConstructAdd support to an unsupported constructAdd support to an unsupported construct

T-CBMCIssue related to an existing CBMC issueIssue related to an existing CBMC issue

Status: Open.

#2543 In model-checking/kani;

· feliperodri opened on Jun 20, 2023

Implement handling of C String

[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.

Status: Open.

#2549 In model-checking/kani;

· celinval opened on Jun 21, 2023

Unit types for external void functions shouldn't be needed

[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.

Status: Open.

#1817 In model-checking/kani;

· adpaco opened on Oct 31, 2022

Enable verification of code that uses C-FFI

[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.

Status: Open.

#2068 In model-checking/kani;

· danielsn opened on Jan 5, 2023

va_arg is currently not supported by kani

[C] BugThis is a bug. Something isn't working.This is a bug. Something isn't working.

Status: Open.

Bug

#2265 In model-checking/kani;

· matthiaskrgr opened on Mar 3, 2023

Reachability analysis cannot see through FFI

[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.

Status: Open.

#3263 In model-checking/kani;

· tautschnig opened on Jun 12, 2024