Adrian Palacios

Results 61 issues of Adrian Palacios

### Description of changes: Changes the conditions to determine whether a property corresponds to a missing function definition. Updates the related UI tests. ### Resolved issues: Resolves #1424 #1271 ###...

### Description of changes: Improves how we extract property attributes, such as property classes. This work was done while working on #1513 but it turns we don't have to use...

Upgrading the CBMC version to 5.59.0 caused regression failures related to missing functions. These are now failing with the description "assertion", apparently because they do not include source locations.

good first issue
Area: User Interface

The following example from `The Rustonomicon/Data Layout/Exotically Sized Types/47.rs` shown below ```rust // compile-flags: --edition 2018 #![allow(unused)] struct MySuperSliceable { info: u32, data: T, } pub fn main() { let...

bug
Area: build
Pri: medium
Type: error
MLP - Should Have

The new parser contains a lot of code which has to do with formatting verification results, locations, etc. There are many improvements that could be made there in terms of...

good first issue
Type: refactor

SIMD intrinsics were disabled in #1143 due to soundness concerns.

Area: verification
Effort: Medium

A significant amount of intrinsics was disabled in #727 because they could not be audited in time. In addition, some intrinsics were unimplemented. The goal is the same, for each...

[C] Internal

The [documentation for the `offset` method](https://doc.rust-lang.org/std/primitive.pointer.html#method.offset) mentions in the safety conditions that: > Both the starting and resulting pointer must be either in bounds or one byte past the end...

Area: verification
Status: blocked

Update `ensure_byte_buf_has_allocated_buffer_member` to include primary allocation so that the code ``` struct aws_byte_buf *buf1 = malloc(sizeof(*buf1)); ensure_byte_buf_has_allocated_buffer_member(buf1); ``` can be replaced by ``` struct aws_byte_buf *buf1 = ensure_byte_buf_has_allocated_buffer_member(buf1); ```

feature-request
cbmc
p3