LAProof.C.cblas.verif_dscal: VST proof for GSL's [cblas_dscal].

Corresponds to C program C/cblas/src/dscal.c.

body_cblas_dscal proves the positive-stride updates described by scal_strided and the kernel's unchanged-array result for incX ≤ 0.

Require Import VST.floyd.proofauto.
From vcfloat Require Import FPStdCompCert FPStdLib.
From LAProof.C Require Import floatlib.
From LAProof.C.cblas Require Import dscal scal_model spec_dscal.

Lemma body_cblas_dscal: semax_body Vprog Gprog f_cblas_dscal cblas_dscal_spec.

In the positive-stride branch, each updated element is a correctly rounded BMULT. Its relative-error bound requires that product to be finite; this is a per-element condition rather than a global accumulation hypothesis.